This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pthaus

Description: The product of a collection of Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion pthaus ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) → ( ∏t ‘ 𝐹 ) ∈ Haus )

Proof

Step Hyp Ref Expression
1 haustop ⊢ ( 𝑥 ∈ Haus → 𝑥 ∈ Top )
2 1 ssriv ⊢ Haus ⊆ Top
3 fss ⊢ ( ( 𝐹 : 𝐴 ⟶ Haus ∧ Haus ⊆ Top ) → 𝐹 : 𝐴 ⟶ Top )
4 2 3 mpan2 ⊢ ( 𝐹 : 𝐴 ⟶ Haus → 𝐹 : 𝐴 ⟶ Top )
5 pttop ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → ( ∏t ‘ 𝐹 ) ∈ Top )
6 4 5 sylan2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) → ( ∏t ‘ 𝐹 ) ∈ Top )
7 simprl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) )
8 eqid ⊢ ( ∏t ‘ 𝐹 ) = ( ∏t ‘ 𝐹 )
9 8 ptuni ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( ∏t ‘ 𝐹 ) )
10 4 9 sylan2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( ∏t ‘ 𝐹 ) )
11 10 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( ∏t ‘ 𝐹 ) )
12 7 11 eleqtrrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝑥 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) )
13 ixpfn ⊢ ( 𝑥 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) → 𝑥 Fn 𝐴 )
14 12 13 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝑥 Fn 𝐴 )
15 simprr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) )
16 15 11 eleqtrrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝑦 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) )
17 ixpfn ⊢ ( 𝑦 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) → 𝑦 Fn 𝐴 )
18 16 17 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝑦 Fn 𝐴 )
19 eqfnfv ⊢ ( ( 𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴 ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑘 ∈ 𝐴 ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
20 14 18 19 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑘 ∈ 𝐴 ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
21 20 necon3abid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ( 𝑥 ≠ 𝑦 ↔ ¬ ∀ 𝑘 ∈ 𝐴 ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
22 rexnal ⊢ ( ∃ 𝑘 ∈ 𝐴 ¬ ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ↔ ¬ ∀ 𝑘 ∈ 𝐴 ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) )
23 df-ne ⊢ ( ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ↔ ¬ ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) )
24 simpllr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → 𝐹 : 𝐴 ⟶ Haus )
25 simprl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → 𝑘 ∈ 𝐴 )
26 24 25 ffvelcdmd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ Haus )
27 vex ⊢ 𝑥 ∈ V
28 27 elixp ⊢ ( 𝑥 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝑥 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑥 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
29 28 simprbi ⊢ ( 𝑥 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) → ∀ 𝑘 ∈ 𝐴 ( 𝑥 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
30 12 29 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ∀ 𝑘 ∈ 𝐴 ( 𝑥 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
31 30 r19.21bi ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
32 31 adantrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → ( 𝑥 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
33 vex ⊢ 𝑦 ∈ V
34 33 elixp ⊢ ( 𝑦 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝑦 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑦 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
35 34 simprbi ⊢ ( 𝑦 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) → ∀ 𝑘 ∈ 𝐴 ( 𝑦 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
36 16 35 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ∀ 𝑘 ∈ 𝐴 ( 𝑦 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
37 36 r19.21bi ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑦 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
38 37 adantrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → ( 𝑦 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
39 simprr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) )
40 eqid ⊢ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 )
41 40 hausnei ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ Haus ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝑦 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → ∃ 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∃ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
42 26 32 38 39 41 syl13anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → ∃ 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∃ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
43 simp-4l ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝐴 ∈ 𝑉 )
44 4 ad4antlr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝐹 : 𝐴 ⟶ Top )
45 25 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝑘 ∈ 𝐴 )
46 eqid ⊢ ∪ ( ∏t ‘ 𝐹 ) = ∪ ( ∏t ‘ 𝐹 )
47 46 8 ptpjcn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝑘 ∈ 𝐴 ) → ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) ∈ ( ( ∏t ‘ 𝐹 ) Cn ( 𝐹 ‘ 𝑘 ) ) )
48 43 44 45 47 syl3anc ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) ∈ ( ( ∏t ‘ 𝐹 ) Cn ( 𝐹 ‘ 𝑘 ) ) )
49 simprll ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) )
50 eqid ⊢ ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) = ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) )
51 50 mptpreima ⊢ ( ◡ ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) “ 𝑚 ) = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 }
52 cnima ⊢ ( ( ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) ∈ ( ( ∏t ‘ 𝐹 ) Cn ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ) → ( ◡ ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) “ 𝑚 ) ∈ ( ∏t ‘ 𝐹 ) )
53 51 52 eqeltrrid ⊢ ( ( ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) ∈ ( ( ∏t ‘ 𝐹 ) Cn ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ) → { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∈ ( ∏t ‘ 𝐹 ) )
54 48 49 53 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∈ ( ∏t ‘ 𝐹 ) )
55 simprlr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) )
56 50 mptpreima ⊢ ( ◡ ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) “ 𝑛 ) = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 }
57 cnima ⊢ ( ( ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) ∈ ( ( ∏t ‘ 𝐹 ) Cn ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) → ( ◡ ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) “ 𝑛 ) ∈ ( ∏t ‘ 𝐹 ) )
58 56 57 eqeltrrid ⊢ ( ( ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) ∈ ( ( ∏t ‘ 𝐹 ) Cn ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) → { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ∈ ( ∏t ‘ 𝐹 ) )
59 48 55 58 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ∈ ( ∏t ‘ 𝐹 ) )
60 fveq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ‘ 𝑘 ) = ( 𝑥 ‘ 𝑘 ) )
61 60 eleq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ↔ ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ) )
62 7 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) )
63 simprr1 ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 )
64 61 62 63 elrabd ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝑥 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } )
65 fveq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) )
66 65 eleq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ↔ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ) )
67 15 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) )
68 simprr2 ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 )
69 66 67 68 elrabd ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝑦 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } )
70 inrab ⊢ ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ) = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ) }
71 simprr3 ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ( 𝑚 ∩ 𝑛 ) = ∅ )
72 inelcm ⊢ ( ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ) → ( 𝑚 ∩ 𝑛 ) ≠ ∅ )
73 72 necon2bi ⊢ ( ( 𝑚 ∩ 𝑛 ) = ∅ → ¬ ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ) )
74 71 73 syl ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ¬ ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ) )
75 74 ralrimivw ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ∀ 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ¬ ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ) )
76 rabeq0 ⊢ ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ) } = ∅ ↔ ∀ 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ¬ ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ) )
77 75 76 sylibr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ) } = ∅ )
78 70 77 eqtrid ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ) = ∅ )
79 eleq2 ⊢ ( 𝑢 = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } → ( 𝑥 ∈ 𝑢 ↔ 𝑥 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ) )
80 ineq1 ⊢ ( 𝑢 = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } → ( 𝑢 ∩ 𝑣 ) = ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ 𝑣 ) )
81 80 eqeq1d ⊢ ( 𝑢 = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } → ( ( 𝑢 ∩ 𝑣 ) = ∅ ↔ ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ 𝑣 ) = ∅ ) )
82 79 81 3anbi13d ⊢ ( 𝑢 = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } → ( ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ↔ ( 𝑥 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∧ 𝑦 ∈ 𝑣 ∧ ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ 𝑣 ) = ∅ ) ) )
83 eleq2 ⊢ ( 𝑣 = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } → ( 𝑦 ∈ 𝑣 ↔ 𝑦 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ) )
84 ineq2 ⊢ ( 𝑣 = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } → ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ 𝑣 ) = ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ) )
85 84 eqeq1d ⊢ ( 𝑣 = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } → ( ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ 𝑣 ) = ∅ ↔ ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ) = ∅ ) )
86 83 85 3anbi23d ⊢ ( 𝑣 = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } → ( ( 𝑥 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∧ 𝑦 ∈ 𝑣 ∧ ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ 𝑣 ) = ∅ ) ↔ ( 𝑥 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∧ 𝑦 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ∧ ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ) = ∅ ) ) )
87 82 86 rspc2ev ⊢ ( ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∈ ( ∏t ‘ 𝐹 ) ∧ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ∈ ( ∏t ‘ 𝐹 ) ∧ ( 𝑥 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∧ 𝑦 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ∧ ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ) = ∅ ) ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
88 54 59 64 69 78 87 syl113anc ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
89 88 expr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )
90 89 rexlimdvva ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → ( ∃ 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∃ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )
91 42 90 mpd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
92 91 expr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )
93 23 92 biimtrrid ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ¬ ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )
94 93 rexlimdva ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ( ∃ 𝑘 ∈ 𝐴 ¬ ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )
95 22 94 biimtrrid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ( ¬ ∀ 𝑘 ∈ 𝐴 ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )
96 21 95 sylbid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )
97 96 ralrimivva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) → ∀ 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∀ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )
98 46 ishaus ⊢ ( ( ∏t ‘ 𝐹 ) ∈ Haus ↔ ( ( ∏t ‘ 𝐹 ) ∈ Top ∧ ∀ 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∀ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) )
99 6 97 98 sylanbrc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) → ( ∏t ‘ 𝐹 ) ∈ Haus )