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 ⊢X=⋃J
qtopt1.1 ⊢φ→J∈Fre
qtopt1.2 ⊢φ→F:X⟶ontoY
qtopt1.3 ⊢φ∧x∈Y→F-1x∈Clsd⁡J
Assertion qtopt1 ⊢φ→JqTopF∈Fre

Proof

Step Hyp Ref Expression
1 qtopt1.x ⊢X=⋃J
2 qtopt1.1 ⊢φ→J∈Fre
3 qtopt1.2 ⊢φ→F:X⟶ontoY
4 qtopt1.3 ⊢φ∧x∈Y→F-1x∈Clsd⁡J
5 t1top ⊢J∈Fre→J∈Top
6 2 5 syl ⊢φ→J∈Top
7 fofn ⊢F:X⟶ontoY→FFnX
8 3 7 syl ⊢φ→FFnX
9 1 qtoptop ⊢J∈Top∧FFnX→JqTopF∈Top
10 6 8 9 syl2anc ⊢φ→JqTopF∈Top
11 simpr ⊢φ∧x∈⋃JqTopF→x∈⋃JqTopF
12 1 qtopuni ⊢J∈Top∧F:X⟶ontoY→Y=⋃JqTopF
13 6 3 12 syl2anc ⊢φ→Y=⋃JqTopF
14 13 adantr ⊢φ∧x∈⋃JqTopF→Y=⋃JqTopF
15 11 14 eleqtrrd ⊢φ∧x∈⋃JqTopF→x∈Y
16 15 snssd ⊢φ∧x∈⋃JqTopF→x⊆Y
17 15 4 syldan ⊢φ∧x∈⋃JqTopF→F-1x∈Clsd⁡J
18 6 1 jctir ⊢φ→J∈Top∧X=⋃J
19 istopon ⊢J∈TopOn⁡X↔J∈Top∧X=⋃J
20 18 19 sylibr ⊢φ→J∈TopOn⁡X
21 qtopcld ⊢J∈TopOn⁡X∧F:X⟶ontoY→x∈Clsd⁡JqTopF↔x⊆Y∧F-1x∈Clsd⁡J
22 20 3 21 syl2anc ⊢φ→x∈Clsd⁡JqTopF↔x⊆Y∧F-1x∈Clsd⁡J
23 22 adantr ⊢φ∧x∈⋃JqTopF→x∈Clsd⁡JqTopF↔x⊆Y∧F-1x∈Clsd⁡J
24 16 17 23 mpbir2and ⊢φ∧x∈⋃JqTopF→x∈Clsd⁡JqTopF
25 24 ralrimiva ⊢φ→∀x∈⋃JqTopFx∈Clsd⁡JqTopF
26 eqid ⊢⋃JqTopF=⋃JqTopF
27 26 ist1 ⊢JqTopF∈Fre↔JqTopF∈Top∧∀x∈⋃JqTopFx∈Clsd⁡JqTopF
28 10 25 27 sylanbrc ⊢φ→JqTopF∈Fre