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 ⟶ onto Y
qtopt1.3 ⊢ φ ∧ x ∈ Y → F -1 x ∈ Clsd ⁡ J
Assertion qtopt1 ⊢ φ → J qTop F ∈ Fre

Proof

Step Hyp Ref Expression
1 qtopt1.x ⊢ X = ⋃ J
2 qtopt1.1 ⊢ φ → J ∈ Fre
3 qtopt1.2 ⊢ φ → F : X ⟶ onto Y
4 qtopt1.3 ⊢ φ ∧ x ∈ Y → F -1 x ∈ Clsd ⁡ J
5 t1top ⊢ J ∈ Fre → J ∈ Top
6 2 5 syl ⊢ φ → J ∈ Top
7 fofn ⊢ F : X ⟶ onto Y → F Fn X
8 3 7 syl ⊢ φ → F Fn X
9 1 qtoptop ⊢ J ∈ Top ∧ F Fn X → J qTop F ∈ Top
10 6 8 9 syl2anc ⊢ φ → J qTop F ∈ Top
11 simpr ⊢ φ ∧ x ∈ ⋃ J qTop F → x ∈ ⋃ J qTop F
12 1 qtopuni ⊢ J ∈ Top ∧ F : X ⟶ onto Y → Y = ⋃ J qTop F
13 6 3 12 syl2anc ⊢ φ → Y = ⋃ J qTop F
14 13 adantr ⊢ φ ∧ x ∈ ⋃ J qTop F → Y = ⋃ J qTop F
15 11 14 eleqtrrd ⊢ φ ∧ x ∈ ⋃ J qTop F → x ∈ Y
16 15 snssd ⊢ φ ∧ x ∈ ⋃ J qTop F → x ⊆ Y
17 15 4 syldan ⊢ φ ∧ x ∈ ⋃ J qTop F → F -1 x ∈ 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 ⟶ onto Y → x ∈ Clsd ⁡ J qTop F ↔ x ⊆ Y ∧ F -1 x ∈ Clsd ⁡ J
22 20 3 21 syl2anc ⊢ φ → x ∈ Clsd ⁡ J qTop F ↔ x ⊆ Y ∧ F -1 x ∈ Clsd ⁡ J
23 22 adantr ⊢ φ ∧ x ∈ ⋃ J qTop F → x ∈ Clsd ⁡ J qTop F ↔ x ⊆ Y ∧ F -1 x ∈ Clsd ⁡ J
24 16 17 23 mpbir2and ⊢ φ ∧ x ∈ ⋃ J qTop F → x ∈ Clsd ⁡ J qTop F
25 24 ralrimiva ⊢ φ → ∀ x ∈ ⋃ J qTop F x ∈ Clsd ⁡ J qTop F
26 eqid ⊢ ⋃ J qTop F = ⋃ J qTop F
27 26 ist1 ⊢ J qTop F ∈ Fre ↔ J qTop F ∈ Top ∧ ∀ x ∈ ⋃ J qTop F x ∈ Clsd ⁡ J qTop F
28 10 25 27 sylanbrc ⊢ φ → J qTop F ∈ Fre