Metamath Proof Explorer

Theorem cnt0

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

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

Proof

Step Hyp Ref Expression
1 cntop1 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
2 1 3ad2ant3 ⊢ ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ Top )
3 simpl3 ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
4 cnima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑤 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑤 ) ∈ 𝐽 )
5 3 4 sylan ⊢ ( ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑤 ) ∈ 𝐽 )
6 eleq2 ⊢ ( 𝑧 = ( ◡ 𝐹 “ 𝑤 ) → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ) )
7 eleq2 ⊢ ( 𝑧 = ( ◡ 𝐹 “ 𝑤 ) → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ) )
8 6 7 bibi12d ⊢ ( 𝑧 = ( ◡ 𝐹 “ 𝑤 ) → ( ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) ↔ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ) ) )
9 8 rspcv ⊢ ( ( ◡ 𝐹 “ 𝑤 ) ∈ 𝐽 → ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ) ) )
10 5 9 syl ⊢ ( ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ) ) )
11 simprl ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝑥 ∈ ∪ 𝐽 )
12 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
13 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
14 12 13 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
15 3 14 syl ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
16 15 ffnd ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝐹 Fn ∪ 𝐽 )
17 elpreima ⊢ ( 𝐹 Fn ∪ 𝐽 → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ ( 𝑥 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ) ) )
18 16 17 syl ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ ( 𝑥 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ) ) )
19 11 18 mpbirand ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ) )
20 simprr ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝑦 ∈ ∪ 𝐽 )
21 elpreima ⊢ ( 𝐹 Fn ∪ 𝐽 → ( 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ ( 𝑦 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) )
22 16 21 syl ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ ( 𝑦 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) )
23 20 22 mpbirand ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) )
24 19 23 bibi12d ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) )
25 24 adantr ⊢ ( ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) )
26 10 25 sylibd ⊢ ( ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) )
27 26 ralrimdva ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → ∀ 𝑤 ∈ 𝐾 ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) )
28 simpl1 ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝐾 ∈ Kol2 )
29 15 11 ffvelrnd ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ∪ 𝐾 )
30 15 20 ffvelrnd ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝐾 )
31 13 t0sep ⊢ ( ( 𝐾 ∈ Kol2 ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ ∪ 𝐾 ∧ ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝐾 ) ) → ( ∀ 𝑤 ∈ 𝐾 ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
32 28 29 30 31 syl12anc ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( ∀ 𝑤 ∈ 𝐾 ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
33 27 32 syld ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
34 simpl2 ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝐹 : 𝑋 –1-1→ 𝑌 )
35 15 fdmd ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → dom 𝐹 = ∪ 𝐽 )
36 f1dm ⊢ ( 𝐹 : 𝑋 –1-1→ 𝑌 → dom 𝐹 = 𝑋 )
37 34 36 syl ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → dom 𝐹 = 𝑋 )
38 35 37 eqtr3d ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ∪ 𝐽 = 𝑋 )
39 11 38 eleqtrd ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝑥 ∈ 𝑋 )
40 20 38 eleqtrd ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝑦 ∈ 𝑋 )
41 f1fveq ⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
42 34 39 40 41 syl12anc ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
43 33 42 sylibd ⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → 𝑥 = 𝑦 ) )
44 43 ralrimivva ⊢ ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → 𝑥 = 𝑦 ) )
45 12 ist0 ⊢ ( 𝐽 ∈ Kol2 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → 𝑥 = 𝑦 ) ) )
46 2 44 45 sylanbrc ⊢ ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ Kol2 )