Metamath Proof Explorer


Theorem ispconn

Description: The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypothesis ispconn.1 X=J
Assertion ispconn JPConnJTopxXyXfIICnJf0=xf1=y

Proof

Step Hyp Ref Expression
1 ispconn.1 X=J
2 unieq j=Jj=J
3 2 1 eqtr4di j=Jj=X
4 oveq2 j=JIICnj=IICnJ
5 4 rexeqdv j=JfIICnjf0=xf1=yfIICnJf0=xf1=y
6 3 5 raleqbidv j=JyjfIICnjf0=xf1=yyXfIICnJf0=xf1=y
7 3 6 raleqbidv j=JxjyjfIICnjf0=xf1=yxXyXfIICnJf0=xf1=y
8 df-pconn PConn=jTop|xjyjfIICnjf0=xf1=y
9 7 8 elrab2 JPConnJTopxXyXfIICnJf0=xf1=y