Metamath Proof Explorer

Theorem qtopt1

Description: If every equivalence class is closed, then the quotient space is T_1 . (Contributed by Thierry Arnoux, 5-Jan-2020)

Ref Expression
Hypotheses qtopt1.x ⊢ 𝑋 = ∪ 𝐽
qtopt1.1 ⊢ ( 𝜑 → 𝐽 ∈ Fre )
qtopt1.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶onto 𝑌 )
qtopt1.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ◡ 𝐹 “ { 𝑥 } ) ∈ ( Clsd ‘ 𝐽 ) )
Assertion qtopt1 ( 𝜑 → ( 𝐽 qTop 𝐹 ) ∈ Fre )

Proof

Step Hyp Ref Expression
1 qtopt1.x ⊢ 𝑋 = ∪ 𝐽
2 qtopt1.1 ⊢ ( 𝜑 → 𝐽 ∈ Fre )
3 qtopt1.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶onto 𝑌 )
4 qtopt1.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ◡ 𝐹 “ { 𝑥 } ) ∈ ( Clsd ‘ 𝐽 ) )
5 t1top ⊢ ( 𝐽 ∈ Fre → 𝐽 ∈ Top )
6 2 5 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
7 fofn ⊢ ( 𝐹 : 𝑋 ⟶onto 𝑌 → 𝐹 Fn 𝑋 )
8 3 7 syl ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
9 1 qtoptop ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ Top )
10 6 8 9 syl2anc ⊢ ( 𝜑 → ( 𝐽 qTop 𝐹 ) ∈ Top )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝐽 qTop 𝐹 ) ) → 𝑥 ∈ ∪ ( 𝐽 qTop 𝐹 ) )
12 1 qtopuni ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋 ⟶onto 𝑌 ) → 𝑌 = ∪ ( 𝐽 qTop 𝐹 ) )
13 6 3 12 syl2anc ⊢ ( 𝜑 → 𝑌 = ∪ ( 𝐽 qTop 𝐹 ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝐽 qTop 𝐹 ) ) → 𝑌 = ∪ ( 𝐽 qTop 𝐹 ) )
15 11 14 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝐽 qTop 𝐹 ) ) → 𝑥 ∈ 𝑌 )
16 15 snssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝐽 qTop 𝐹 ) ) → { 𝑥 } ⊆ 𝑌 )
17 15 4 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝐽 qTop 𝐹 ) ) → ( ◡ 𝐹 “ { 𝑥 } ) ∈ ( Clsd ‘ 𝐽 ) )
18 6 1 jctir ⊢ ( 𝜑 → ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐽 ) )
19 istopon ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ↔ ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐽 ) )
20 18 19 sylibr ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
21 qtopcld ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶onto 𝑌 ) → ( { 𝑥 } ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) ↔ ( { 𝑥 } ⊆ 𝑌 ∧ ( ◡ 𝐹 “ { 𝑥 } ) ∈ ( Clsd ‘ 𝐽 ) ) ) )
22 20 3 21 syl2anc ⊢ ( 𝜑 → ( { 𝑥 } ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) ↔ ( { 𝑥 } ⊆ 𝑌 ∧ ( ◡ 𝐹 “ { 𝑥 } ) ∈ ( Clsd ‘ 𝐽 ) ) ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝐽 qTop 𝐹 ) ) → ( { 𝑥 } ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) ↔ ( { 𝑥 } ⊆ 𝑌 ∧ ( ◡ 𝐹 “ { 𝑥 } ) ∈ ( Clsd ‘ 𝐽 ) ) ) )
24 16 17 23 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝐽 qTop 𝐹 ) ) → { 𝑥 } ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) )
25 24 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ∪ ( 𝐽 qTop 𝐹 ) { 𝑥 } ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) )
26 eqid ⊢ ∪ ( 𝐽 qTop 𝐹 ) = ∪ ( 𝐽 qTop 𝐹 )
27 26 ist1 ⊢ ( ( 𝐽 qTop 𝐹 ) ∈ Fre ↔ ( ( 𝐽 qTop 𝐹 ) ∈ Top ∧ ∀ 𝑥 ∈ ∪ ( 𝐽 qTop 𝐹 ) { 𝑥 } ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) ) )
28 10 25 27 sylanbrc ⊢ ( 𝜑 → ( 𝐽 qTop 𝐹 ) ∈ Fre )