Theorem qtoppconn

Description: A quotient of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015)

	Ref	Expression
Hypothesis	pconnpi1.x	⊢ 𝑋 = ∪ 𝐽
Assertion	qtoppconn	⊢ ( ( 𝐽 ∈ PConn ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ PConn )

Proof

Step	Hyp	Ref	Expression
1		pconnpi1.x	⊢ 𝑋 = ∪ 𝐽
2		pconntop	⊢ ( 𝐽 ∈ PConn → 𝐽 ∈ Top )
3		eqid	⊢ ∪ ( 𝐽 qTop 𝐹 ) = ∪ ( 𝐽 qTop 𝐹 )
4	3	cnpconn	⊢ ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ ∪ ( 𝐽 qTop 𝐹 ) ∧ 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) ) → ( 𝐽 qTop 𝐹 ) ∈ PConn )
5	1 2 4	qtopcmplem	⊢ ( ( 𝐽 ∈ PConn ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ PConn )