Theorem qustps

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

	Ref	Expression
Hypotheses	qustps.u	|- ( ph -> U = ( R /s E ) )
	qustps.v	|- ( ph -> V = ( Base ` R ) )
	qustps.e	|- ( ph -> E e. W )
	qustps.r	|- ( ph -> R e. TopSp )
Assertion	qustps	|- ( ph -> U e. TopSp )

Proof

Step	Hyp	Ref	Expression
1		qustps.u	|- ( ph -> U = ( R /s E ) )
2		qustps.v	|- ( ph -> V = ( Base ` R ) )
3		qustps.e	|- ( ph -> E e. W )
4		qustps.r	|- ( ph -> R e. TopSp )
5		eqid	|- ( x e. V |-> [ x ] E ) = ( x e. V |-> [ x ] E )
6	1 2 5 3 4	qusval	|- ( ph -> U = ( ( x e. V |-> [ x ] E ) "s R ) )
7	1 2 5 3 4	quslem	|- ( ph -> ( x e. V |-> [ x ] E ) : V -onto-> ( V /. E ) )
8	6 2 7 4	imastps	|- ( ph -> U e. TopSp )