Metamath Proof Explorer

Theorem pconncn

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

Ref Expression
Hypothesis ispconn.1 
|- X = U. J
Assertion pconncn 
|- ( ( J e. PConn /\ A e. X /\ B e. X ) -> E. f e. ( II Cn J ) ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) )

Proof

Step Hyp Ref Expression
1 ispconn.1 
 |-  X = U. J
2 1 ispconn 
 |-  ( J e. PConn <-> ( J e. Top /\ A. x e. X A. y e. X E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) ) )
3 2 simprbi 
 |-  ( J e. PConn -> A. x e. X A. y e. X E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
4 eqeq2 
 |-  ( x = A -> ( ( f ` 0 ) = x <-> ( f ` 0 ) = A ) )
5 4 anbi1d 
 |-  ( x = A -> ( ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) <-> ( ( f ` 0 ) = A /\ ( f ` 1 ) = y ) ) )
6 5 rexbidv 
 |-  ( x = A -> ( E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) <-> E. f e. ( II Cn J ) ( ( f ` 0 ) = A /\ ( f ` 1 ) = y ) ) )
7 eqeq2 
 |-  ( y = B -> ( ( f ` 1 ) = y <-> ( f ` 1 ) = B ) )
8 7 anbi2d 
 |-  ( y = B -> ( ( ( f ` 0 ) = A /\ ( f ` 1 ) = y ) <-> ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) )
9 8 rexbidv 
 |-  ( y = B -> ( E. f e. ( II Cn J ) ( ( f ` 0 ) = A /\ ( f ` 1 ) = y ) <-> E. f e. ( II Cn J ) ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) )
10 6 9 rspc2v 
 |-  ( ( A e. X /\ B e. X ) -> ( A. x e. X A. y e. X E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) -> E. f e. ( II Cn J ) ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) )
11 3 10 syl5com 
 |-  ( J e. PConn -> ( ( A e. X /\ B e. X ) -> E. f e. ( II Cn J ) ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) )
12 11 3impib 
 |-  ( ( J e. PConn /\ A e. X /\ B e. X ) -> E. f e. ( II Cn J ) ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) )