Metamath Proof Explorer

Theorem cnt1

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

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

Proof

Step Hyp Ref Expression
1 cntop1 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
2 1 3ad2ant3 ⊢ ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ Top )
3 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
4 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
5 3 4 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
6 5 3ad2ant3 ⊢ ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
7 6 ffnd ⊢ ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 Fn ∪ 𝐽 )
8 fnsnfv ⊢ ( ( 𝐹 Fn ∪ 𝐽 ∧ 𝑥 ∈ ∪ 𝐽 ) → { ( 𝐹 ‘ 𝑥 ) } = ( 𝐹 “ { 𝑥 } ) )
9 7 8 sylan ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ∪ 𝐽 ) → { ( 𝐹 ‘ 𝑥 ) } = ( 𝐹 “ { 𝑥 } ) )
10 9 imaeq2d ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) = ( ◡ 𝐹 “ ( 𝐹 “ { 𝑥 } ) ) )
11 simpl2 ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝐹 : 𝑋 –1-1→ 𝑌 )
12 6 fdmd ⊢ ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → dom 𝐹 = ∪ 𝐽 )
13 f1dm ⊢ ( 𝐹 : 𝑋 –1-1→ 𝑌 → dom 𝐹 = 𝑋 )
14 13 3ad2ant2 ⊢ ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → dom 𝐹 = 𝑋 )
15 12 14 eqtr3d ⊢ ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ∪ 𝐽 = 𝑋 )
16 15 eleq2d ⊢ ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑥 ∈ ∪ 𝐽 ↔ 𝑥 ∈ 𝑋 ) )
17 16 biimpa ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝑥 ∈ 𝑋 )
18 17 snssd ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ∪ 𝐽 ) → { 𝑥 } ⊆ 𝑋 )
19 f1imacnv ⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ { 𝑥 } ⊆ 𝑋 ) → ( ◡ 𝐹 “ ( 𝐹 “ { 𝑥 } ) ) = { 𝑥 } )
20 11 18 19 syl2anc ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ◡ 𝐹 “ ( 𝐹 “ { 𝑥 } ) ) = { 𝑥 } )
21 10 20 eqtrd ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) = { 𝑥 } )
22 simpl3 ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
23 simpl1 ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝐾 ∈ Fre )
24 6 ffvelrnda ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ( 𝐹 ‘ 𝑥 ) ∈ ∪ 𝐾 )
25 4 t1sncld ⊢ ( ( 𝐾 ∈ Fre ∧ ( 𝐹 ‘ 𝑥 ) ∈ ∪ 𝐾 ) → { ( 𝐹 ‘ 𝑥 ) } ∈ ( Clsd ‘ 𝐾 ) )
26 23 24 25 syl2anc ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ∪ 𝐽 ) → { ( 𝐹 ‘ 𝑥 ) } ∈ ( Clsd ‘ 𝐾 ) )
27 cnclima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ { ( 𝐹 ‘ 𝑥 ) } ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ∈ ( Clsd ‘ 𝐽 ) )
28 22 26 27 syl2anc ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ∈ ( Clsd ‘ 𝐽 ) )
29 21 28 eqeltrrd ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ∪ 𝐽 ) → { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) )
30 29 ralrimiva ⊢ ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ∀ 𝑥 ∈ ∪ 𝐽 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) )
31 3 ist1 ⊢ ( 𝐽 ∈ Fre ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ ∪ 𝐽 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) ) )
32 2 30 31 sylanbrc ⊢ ( ( 𝐾 ∈ Fre ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ Fre )