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=BaseR
qustps.e φEW
qustps.r φRTopSp
Assertion qustps φUTopSp

Proof

Step Hyp Ref Expression
1 qustps.u φU=R/𝑠E
2 qustps.v φV=BaseR
3 qustps.e φEW
4 qustps.r φRTopSp
5 eqid xVxE=xVxE
6 1 2 5 3 4 qusval φU=xVxE𝑠R
7 1 2 5 3 4 quslem φxVxE:VontoV/E
8 6 2 7 4 imastps φUTopSp