Metamath Proof Explorer

Theorem cnhaus

Description: The preimage of a Hausdorff topology under an injective map is Hausdorff. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion cnhaus ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ Haus )

Proof

Step Hyp Ref Expression
1 cntop1 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
2 1 3ad2ant3 ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ Top )
3 simpl1 ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐾 ∈ Haus )
4 simpl3 ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
5 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
6 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
7 5 6 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
8 4 7 syl ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
9 simprll ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ ∪ 𝐽 )
10 8 9 ffvelcdmd ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ∪ 𝐾 )
11 simprlr ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑦 ∈ ∪ 𝐽 )
12 8 11 ffvelcdmd ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝐾 )
13 simprr ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ≠ 𝑦 )
14 simpl2 ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐹 : 𝑋 –1-1→ 𝑌 )
15 8 fdmd ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → dom 𝐹 = ∪ 𝐽 )
16 f1dm ⊢ ( 𝐹 : 𝑋 –1-1→ 𝑌 → dom 𝐹 = 𝑋 )
17 14 16 syl ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → dom 𝐹 = 𝑋 )
18 15 17 eqtr3d ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → ∪ 𝐽 = 𝑋 )
19 9 18 eleqtrd ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ 𝑋 )
20 11 18 eleqtrd ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑦 ∈ 𝑋 )
21 f1fveq ⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
22 14 19 20 21 syl12anc ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
23 22 necon3bid ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ 𝑥 ≠ 𝑦 ) )
24 13 23 mpbird ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) )
25 6 hausnei ⊢ ( ( 𝐾 ∈ Haus ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ ∪ 𝐾 ∧ ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝐾 ∧ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ) → ∃ 𝑢 ∈ 𝐾 ∃ 𝑣 ∈ 𝐾 ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
26 3 10 12 24 25 syl13anc ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → ∃ 𝑢 ∈ 𝐾 ∃ 𝑣 ∈ 𝐾 ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
27 simpll3 ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
28 simprll ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑢 ∈ 𝐾 )
29 cnima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑢 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑢 ) ∈ 𝐽 )
30 27 28 29 syl2anc ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ◡ 𝐹 “ 𝑢 ) ∈ 𝐽 )
31 simprlr ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑣 ∈ 𝐾 )
32 cnima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑣 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑣 ) ∈ 𝐽 )
33 27 31 32 syl2anc ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ◡ 𝐹 “ 𝑣 ) ∈ 𝐽 )
34 9 adantr ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑥 ∈ ∪ 𝐽 )
35 simprr1 ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 )
36 8 adantr ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
37 36 ffnd ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝐹 Fn ∪ 𝐽 )
38 elpreima ⊢ ( 𝐹 Fn ∪ 𝐽 → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑢 ) ↔ ( 𝑥 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ) ) )
39 37 38 syl ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑢 ) ↔ ( 𝑥 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ) ) )
40 34 35 39 mpbir2and ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑥 ∈ ( ◡ 𝐹 “ 𝑢 ) )
41 11 adantr ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑦 ∈ ∪ 𝐽 )
42 simprr2 ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 )
43 elpreima ⊢ ( 𝐹 Fn ∪ 𝐽 → ( 𝑦 ∈ ( ◡ 𝐹 “ 𝑣 ) ↔ ( 𝑦 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ) ) )
44 37 43 syl ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 𝑦 ∈ ( ◡ 𝐹 “ 𝑣 ) ↔ ( 𝑦 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ) ) )
45 41 42 44 mpbir2and ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑦 ∈ ( ◡ 𝐹 “ 𝑣 ) )
46 ffun ⊢ ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 → Fun 𝐹 )
47 inpreima ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) = ( ( ◡ 𝐹 “ 𝑢 ) ∩ ( ◡ 𝐹 “ 𝑣 ) ) )
48 36 46 47 3syl ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) = ( ( ◡ 𝐹 “ 𝑢 ) ∩ ( ◡ 𝐹 “ 𝑣 ) ) )
49 simprr3 ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 𝑢 ∩ 𝑣 ) = ∅ )
50 49 imaeq2d ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) = ( ◡ 𝐹 “ ∅ ) )
51 ima0 ⊢ ( ◡ 𝐹 “ ∅ ) = ∅
52 50 51 eqtrdi ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) = ∅ )
53 48 52 eqtr3d ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ( ◡ 𝐹 “ 𝑢 ) ∩ ( ◡ 𝐹 “ 𝑣 ) ) = ∅ )
54 eleq2 ⊢ ( 𝑚 = ( ◡ 𝐹 “ 𝑢 ) → ( 𝑥 ∈ 𝑚 ↔ 𝑥 ∈ ( ◡ 𝐹 “ 𝑢 ) ) )
55 ineq1 ⊢ ( 𝑚 = ( ◡ 𝐹 “ 𝑢 ) → ( 𝑚 ∩ 𝑛 ) = ( ( ◡ 𝐹 “ 𝑢 ) ∩ 𝑛 ) )
56 55 eqeq1d ⊢ ( 𝑚 = ( ◡ 𝐹 “ 𝑢 ) → ( ( 𝑚 ∩ 𝑛 ) = ∅ ↔ ( ( ◡ 𝐹 “ 𝑢 ) ∩ 𝑛 ) = ∅ ) )
57 54 56 3anbi13d ⊢ ( 𝑚 = ( ◡ 𝐹 “ 𝑢 ) → ( ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ↔ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑦 ∈ 𝑛 ∧ ( ( ◡ 𝐹 “ 𝑢 ) ∩ 𝑛 ) = ∅ ) ) )
58 eleq2 ⊢ ( 𝑛 = ( ◡ 𝐹 “ 𝑣 ) → ( 𝑦 ∈ 𝑛 ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑣 ) ) )
59 ineq2 ⊢ ( 𝑛 = ( ◡ 𝐹 “ 𝑣 ) → ( ( ◡ 𝐹 “ 𝑢 ) ∩ 𝑛 ) = ( ( ◡ 𝐹 “ 𝑢 ) ∩ ( ◡ 𝐹 “ 𝑣 ) ) )
60 59 eqeq1d ⊢ ( 𝑛 = ( ◡ 𝐹 “ 𝑣 ) → ( ( ( ◡ 𝐹 “ 𝑢 ) ∩ 𝑛 ) = ∅ ↔ ( ( ◡ 𝐹 “ 𝑢 ) ∩ ( ◡ 𝐹 “ 𝑣 ) ) = ∅ ) )
61 58 60 3anbi23d ⊢ ( 𝑛 = ( ◡ 𝐹 “ 𝑣 ) → ( ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑦 ∈ 𝑛 ∧ ( ( ◡ 𝐹 “ 𝑢 ) ∩ 𝑛 ) = ∅ ) ↔ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑦 ∈ ( ◡ 𝐹 “ 𝑣 ) ∧ ( ( ◡ 𝐹 “ 𝑢 ) ∩ ( ◡ 𝐹 “ 𝑣 ) ) = ∅ ) ) )
62 57 61 rspc2ev ⊢ ( ( ( ◡ 𝐹 “ 𝑢 ) ∈ 𝐽 ∧ ( ◡ 𝐹 “ 𝑣 ) ∈ 𝐽 ∧ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑦 ∈ ( ◡ 𝐹 “ 𝑣 ) ∧ ( ( ◡ 𝐹 “ 𝑢 ) ∩ ( ◡ 𝐹 “ 𝑣 ) ) = ∅ ) ) → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
63 30 33 40 45 53 62 syl113anc ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
64 63 expr ⊢ ( ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
65 64 rexlimdvva ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( ∃ 𝑢 ∈ 𝐾 ∃ 𝑣 ∈ 𝐾 ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
66 26 65 mpd ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑥 ≠ 𝑦 ) ) → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
67 66 expr ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
68 67 ralrimivva ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
69 5 ishaus ⊢ ( 𝐽 ∈ Haus ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
70 2 68 69 sylanbrc ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ Haus )