Theorem qustps

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

	Ref	Expression
Hypotheses	qustps.u	⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s 𝐸 ) )
	qustps.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
	qustps.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
	qustps.r	⊢ ( 𝜑 → 𝑅 ∈ TopSp )
Assertion	qustps	⊢ ( 𝜑 → 𝑈 ∈ TopSp )

Proof

Step	Hyp	Ref	Expression
1		qustps.u	⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s 𝐸 ) )
2		qustps.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3		qustps.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
4		qustps.r	⊢ ( 𝜑 → 𝑅 ∈ TopSp )
5		eqid	⊢ ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] 𝐸 ) = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] 𝐸 )
6	1 2 5 3 4	qusval	⊢ ( 𝜑 → 𝑈 = ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] 𝐸 ) “s 𝑅 ) )
7	1 2 5 3 4	quslem	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] 𝐸 ) : 𝑉 –onto→ ( 𝑉 / 𝐸 ) )
8	6 2 7 4	imastps	⊢ ( 𝜑 → 𝑈 ∈ TopSp )