This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qustps

Description: A quotient structure is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypotheses qustps.u ⊢ φ → U = R / 𝑠 E
qustps.v ⊢ φ → V = Base R
qustps.e ⊢ φ → E ∈ W
qustps.r ⊢ φ → R ∈ TopSp
Assertion qustps ⊢ φ → U ∈ TopSp

Proof

Step Hyp Ref Expression
1 qustps.u ⊢ φ → U = R / 𝑠 E
2 qustps.v ⊢ φ → V = Base R
3 qustps.e ⊢ φ → E ∈ W
4 qustps.r ⊢ φ → R ∈ TopSp
5 eqid ⊢ x ∈ V ⟼ x E = x ∈ V ⟼ x E
6 1 2 5 3 4 qusval ⊢ φ → U = x ∈ V ⟼ x E “ 𝑠 R
7 1 2 5 3 4 quslem ⊢ φ → x ∈ V ⟼ x E : V ⟶ onto V / E
8 6 2 7 4 imastps ⊢ φ → U ∈ TopSp