Theorem qustps

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

	Ref	Expression
Hypotheses	qustps.u	$$⊢\phi \to U=R{/}_{𝑠}E$$
	qustps.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	qustps.e	$$⊢\phi \to E\in W$$
	qustps.r	$$⊢\phi \to R\in \mathrm{TopSp}$$
Assertion	qustps	$$⊢\phi \to U\in \mathrm{TopSp}$$

Proof

Step	Hyp	Ref	Expression
1		qustps.u	$$⊢\phi \to U=R{/}_{𝑠}E$$
2		qustps.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
3		qustps.e	$$⊢\phi \to E\in W$$
4		qustps.r	$$⊢\phi \to R\in \mathrm{TopSp}$$
5		eqid	$$⊢\left(x\in V⟼\left[x\right]E\right)=\left(x\in V⟼\left[x\right]E\right)$$
6	1 2 5 3 4	qusval	$$⊢\phi \to U=\left(x\in V⟼\left[x\right]E\right){“}_{𝑠}R$$
7	1 2 5 3 4	quslem	$$⊢\phi \to \left(x\in V⟼\left[x\right]E\right):V\underset{onto}{⟶}V/E$$
8	6 2 7 4	imastps	$$⊢\phi \to U\in \mathrm{TopSp}$$