Theorem qtopconn

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

	Ref	Expression
Hypothesis	qtopcmp.1	⊢ 𝑋 = ∪ 𝐽
Assertion	qtopconn	⊢ ( ( 𝐽 ∈ Conn ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ Conn )

Proof

Step	Hyp	Ref	Expression
1		qtopcmp.1	⊢ 𝑋 = ∪ 𝐽
2		conntop	⊢ ( 𝐽 ∈ Conn → 𝐽 ∈ Top )
3		eqid	⊢ ∪ ( 𝐽 qTop 𝐹 ) = ∪ ( 𝐽 qTop 𝐹 )
4	3	cnconn	⊢ ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ ∪ ( 𝐽 qTop 𝐹 ) ∧ 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) ) → ( 𝐽 qTop 𝐹 ) ∈ Conn )
5	1 2 4	qtopcmplem	⊢ ( ( 𝐽 ∈ Conn ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ Conn )