Metamath Proof Explorer


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 X=J
Assertion qtoppconn JPConnFFnXJqTopFPConn

Proof

Step Hyp Ref Expression
1 pconnpi1.x X=J
2 pconntop JPConnJTop
3 eqid JqTopF=JqTopF
4 3 cnpconn JPConnF:XontoJqTopFFJCnJqTopFJqTopFPConn
5 1 2 4 qtopcmplem JPConnFFnXJqTopFPConn