Metamath Proof Explorer


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 )