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 )