Metamath Proof Explorer

Theorem qtoptopon

Description: The base set of the quotient topology. (Contributed by Mario Carneiro, 22-Aug-2015)

Ref Expression
Assertion qtoptopon ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y → J qTop F ∈ TopOn ⁡ Y

Proof

Step Hyp Ref Expression
1 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
2 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
3 foeq2 ⊢ X = ⋃ J → F : X ⟶ onto Y ↔ F : ⋃ J ⟶ onto Y
4 2 3 syl ⊢ J ∈ TopOn ⁡ X → F : X ⟶ onto Y ↔ F : ⋃ J ⟶ onto Y
5 4 biimpa ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y → F : ⋃ J ⟶ onto Y
6 fofn ⊢ F : ⋃ J ⟶ onto Y → F Fn ⋃ J
7 5 6 syl ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y → F Fn ⋃ J
8 eqid ⊢ ⋃ J = ⋃ J
9 8 qtoptop ⊢ J ∈ Top ∧ F Fn ⋃ J → J qTop F ∈ Top
10 1 7 9 syl2an2r ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y → J qTop F ∈ Top
11 8 qtopuni ⊢ J ∈ Top ∧ F : ⋃ J ⟶ onto Y → Y = ⋃ J qTop F
12 1 5 11 syl2an2r ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y → Y = ⋃ J qTop F
13 istopon ⊢ J qTop F ∈ TopOn ⁡ Y ↔ J qTop F ∈ Top ∧ Y = ⋃ J qTop F
14 10 12 13 sylanbrc ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y → J qTop F ∈ TopOn ⁡ Y