Metamath Proof Explorer

Theorem elqtop3

Description: Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015)

Ref Expression
Assertion elqtop3 ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y → A ∈ J qTop F ↔ A ⊆ Y ∧ F -1 A ∈ J

Proof

Step Hyp Ref Expression
1 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
2 eqimss ⊢ X = ⋃ J → X ⊆ ⋃ J
3 1 2 syl ⊢ J ∈ TopOn ⁡ X → X ⊆ ⋃ J
4 3 adantr ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y → X ⊆ ⋃ J
5 eqid ⊢ ⋃ J = ⋃ J
6 5 elqtop ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y ∧ X ⊆ ⋃ J → A ∈ J qTop F ↔ A ⊆ Y ∧ F -1 A ∈ J
7 4 6 mpd3an3 ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y → A ∈ J qTop F ↔ A ⊆ Y ∧ F -1 A ∈ J