Metamath Proof Explorer

Theorem txpconn

Description: The topological product of two path-connected spaces is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Assertion txpconn 
|- ( ( R e. PConn /\ S e. PConn ) -> ( R tX S ) e. PConn )

Proof

Step Hyp Ref Expression
1 pconntop 
 |-  ( R e. PConn -> R e. Top )
2 pconntop 
 |-  ( S e. PConn -> S e. Top )
3 txtop 
 |-  ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. Top )
4 1 2 3 syl2an 
 |-  ( ( R e. PConn /\ S e. PConn ) -> ( R tX S ) e. Top )
5 an6 
 |-  ( ( ( R e. PConn /\ x e. U. R /\ z e. U. R ) /\ ( S e. PConn /\ y e. U. S /\ w e. U. S ) ) <-> ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) )
6 eqid 
 |-  U. R = U. R
7 6 pconncn 
 |-  ( ( R e. PConn /\ x e. U. R /\ z e. U. R ) -> E. g e. ( II Cn R ) ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) )
8 eqid 
 |-  U. S = U. S
9 8 pconncn 
 |-  ( ( S e. PConn /\ y e. U. S /\ w e. U. S ) -> E. h e. ( II Cn S ) ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) )
10 7 9 anim12i 
 |-  ( ( ( R e. PConn /\ x e. U. R /\ z e. U. R ) /\ ( S e. PConn /\ y e. U. S /\ w e. U. S ) ) -> ( E. g e. ( II Cn R ) ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ E. h e. ( II Cn S ) ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) )
11 5 10 sylbir 
 |-  ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) -> ( E. g e. ( II Cn R ) ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ E. h e. ( II Cn S ) ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) )
12 reeanv 
 |-  ( E. g e. ( II Cn R ) E. h e. ( II Cn S ) ( ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) <-> ( E. g e. ( II Cn R ) ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ E. h e. ( II Cn S ) ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) )
13 11 12 sylibr 
 |-  ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) -> E. g e. ( II Cn R ) E. h e. ( II Cn S ) ( ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) )
14 iiuni 
 |-  ( 0 [,] 1 ) = U. II
15 eqid 
 |-  ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) = ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. )
16 14 15 txcnmpt 
 |-  ( ( g e. ( II Cn R ) /\ h e. ( II Cn S ) ) -> ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) e. ( II Cn ( R tX S ) ) )
17 16 ad2antrl 
 |-  ( ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) /\ ( ( g e. ( II Cn R ) /\ h e. ( II Cn S ) ) /\ ( ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) ) ) -> ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) e. ( II Cn ( R tX S ) ) )
18 0elunit 
 |-  0 e. ( 0 [,] 1 )
19 fveq2 
 |-  ( t = 0 -> ( g ` t ) = ( g ` 0 ) )
20 fveq2 
 |-  ( t = 0 -> ( h ` t ) = ( h ` 0 ) )
21 19 20 opeq12d 
 |-  ( t = 0 -> <. ( g ` t ) , ( h ` t ) >. = <. ( g ` 0 ) , ( h ` 0 ) >. )
22 opex 
 |-  <. ( g ` 0 ) , ( h ` 0 ) >. e. _V
23 21 15 22 fvmpt 
 |-  ( 0 e. ( 0 [,] 1 ) -> ( ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) ` 0 ) = <. ( g ` 0 ) , ( h ` 0 ) >. )
24 18 23 ax-mp 
 |-  ( ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) ` 0 ) = <. ( g ` 0 ) , ( h ` 0 ) >.
25 simprrl 
 |-  ( ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) /\ ( ( g e. ( II Cn R ) /\ h e. ( II Cn S ) ) /\ ( ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) ) ) -> ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) )
26 25 simpld 
 |-  ( ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) /\ ( ( g e. ( II Cn R ) /\ h e. ( II Cn S ) ) /\ ( ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) ) ) -> ( g ` 0 ) = x )
27 simprrr 
 |-  ( ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) /\ ( ( g e. ( II Cn R ) /\ h e. ( II Cn S ) ) /\ ( ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) ) ) -> ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) )
28 27 simpld 
 |-  ( ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) /\ ( ( g e. ( II Cn R ) /\ h e. ( II Cn S ) ) /\ ( ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) ) ) -> ( h ` 0 ) = y )
29 26 28 opeq12d 
 |-  ( ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) /\ ( ( g e. ( II Cn R ) /\ h e. ( II Cn S ) ) /\ ( ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) ) ) -> <. ( g ` 0 ) , ( h ` 0 ) >. = <. x , y >. )
30 24 29 syl5eq 
 |-  ( ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) /\ ( ( g e. ( II Cn R ) /\ h e. ( II Cn S ) ) /\ ( ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) ) ) -> ( ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) ` 0 ) = <. x , y >. )
31 1elunit 
 |-  1 e. ( 0 [,] 1 )
32 fveq2 
 |-  ( t = 1 -> ( g ` t ) = ( g ` 1 ) )
33 fveq2 
 |-  ( t = 1 -> ( h ` t ) = ( h ` 1 ) )
34 32 33 opeq12d 
 |-  ( t = 1 -> <. ( g ` t ) , ( h ` t ) >. = <. ( g ` 1 ) , ( h ` 1 ) >. )
35 opex 
 |-  <. ( g ` 1 ) , ( h ` 1 ) >. e. _V
36 34 15 35 fvmpt 
 |-  ( 1 e. ( 0 [,] 1 ) -> ( ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) ` 1 ) = <. ( g ` 1 ) , ( h ` 1 ) >. )
37 31 36 ax-mp 
 |-  ( ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) ` 1 ) = <. ( g ` 1 ) , ( h ` 1 ) >.
38 25 simprd 
 |-  ( ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) /\ ( ( g e. ( II Cn R ) /\ h e. ( II Cn S ) ) /\ ( ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) ) ) -> ( g ` 1 ) = z )
39 27 simprd 
 |-  ( ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) /\ ( ( g e. ( II Cn R ) /\ h e. ( II Cn S ) ) /\ ( ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) ) ) -> ( h ` 1 ) = w )
40 38 39 opeq12d 
 |-  ( ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) /\ ( ( g e. ( II Cn R ) /\ h e. ( II Cn S ) ) /\ ( ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) ) ) -> <. ( g ` 1 ) , ( h ` 1 ) >. = <. z , w >. )
41 37 40 syl5eq 
 |-  ( ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) /\ ( ( g e. ( II Cn R ) /\ h e. ( II Cn S ) ) /\ ( ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) ) ) -> ( ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) ` 1 ) = <. z , w >. )
42 fveq1 
 |-  ( f = ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) -> ( f ` 0 ) = ( ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) ` 0 ) )
43 42 eqeq1d 
 |-  ( f = ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) -> ( ( f ` 0 ) = <. x , y >. <-> ( ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) ` 0 ) = <. x , y >. ) )
44 fveq1 
 |-  ( f = ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) -> ( f ` 1 ) = ( ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) ` 1 ) )
45 44 eqeq1d 
 |-  ( f = ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) -> ( ( f ` 1 ) = <. z , w >. <-> ( ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) ` 1 ) = <. z , w >. ) )
46 43 45 anbi12d 
 |-  ( f = ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) -> ( ( ( f ` 0 ) = <. x , y >. /\ ( f ` 1 ) = <. z , w >. ) <-> ( ( ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) ` 0 ) = <. x , y >. /\ ( ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) ` 1 ) = <. z , w >. ) ) )
47 46 rspcev 
 |-  ( ( ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) e. ( II Cn ( R tX S ) ) /\ ( ( ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) ` 0 ) = <. x , y >. /\ ( ( t e. ( 0 [,] 1 ) |-> <. ( g ` t ) , ( h ` t ) >. ) ` 1 ) = <. z , w >. ) ) -> E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = <. x , y >. /\ ( f ` 1 ) = <. z , w >. ) )
48 17 30 41 47 syl12anc 
 |-  ( ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) /\ ( ( g e. ( II Cn R ) /\ h e. ( II Cn S ) ) /\ ( ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) ) ) -> E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = <. x , y >. /\ ( f ` 1 ) = <. z , w >. ) )
49 48 expr 
 |-  ( ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) /\ ( g e. ( II Cn R ) /\ h e. ( II Cn S ) ) ) -> ( ( ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) -> E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = <. x , y >. /\ ( f ` 1 ) = <. z , w >. ) ) )
50 49 rexlimdvva 
 |-  ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) -> ( E. g e. ( II Cn R ) E. h e. ( II Cn S ) ( ( ( g ` 0 ) = x /\ ( g ` 1 ) = z ) /\ ( ( h ` 0 ) = y /\ ( h ` 1 ) = w ) ) -> E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = <. x , y >. /\ ( f ` 1 ) = <. z , w >. ) ) )
51 13 50 mpd 
 |-  ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) /\ ( z e. U. R /\ w e. U. S ) ) -> E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = <. x , y >. /\ ( f ` 1 ) = <. z , w >. ) )
52 51 3expa 
 |-  ( ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) ) /\ ( z e. U. R /\ w e. U. S ) ) -> E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = <. x , y >. /\ ( f ` 1 ) = <. z , w >. ) )
53 52 ralrimivva 
 |-  ( ( ( R e. PConn /\ S e. PConn ) /\ ( x e. U. R /\ y e. U. S ) ) -> A. z e. U. R A. w e. U. S E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = <. x , y >. /\ ( f ` 1 ) = <. z , w >. ) )
54 53 ralrimivva 
 |-  ( ( R e. PConn /\ S e. PConn ) -> A. x e. U. R A. y e. U. S A. z e. U. R A. w e. U. S E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = <. x , y >. /\ ( f ` 1 ) = <. z , w >. ) )
55 eqeq2 
 |-  ( v = <. z , w >. -> ( ( f ` 1 ) = v <-> ( f ` 1 ) = <. z , w >. ) )
56 55 anbi2d 
 |-  ( v = <. z , w >. -> ( ( ( f ` 0 ) = u /\ ( f ` 1 ) = v ) <-> ( ( f ` 0 ) = u /\ ( f ` 1 ) = <. z , w >. ) ) )
57 56 rexbidv 
 |-  ( v = <. z , w >. -> ( E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = u /\ ( f ` 1 ) = v ) <-> E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = u /\ ( f ` 1 ) = <. z , w >. ) ) )
58 57 ralxp 
 |-  ( A. v e. ( U. R X. U. S ) E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = u /\ ( f ` 1 ) = v ) <-> A. z e. U. R A. w e. U. S E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = u /\ ( f ` 1 ) = <. z , w >. ) )
59 eqeq2 
 |-  ( u = <. x , y >. -> ( ( f ` 0 ) = u <-> ( f ` 0 ) = <. x , y >. ) )
60 59 anbi1d 
 |-  ( u = <. x , y >. -> ( ( ( f ` 0 ) = u /\ ( f ` 1 ) = <. z , w >. ) <-> ( ( f ` 0 ) = <. x , y >. /\ ( f ` 1 ) = <. z , w >. ) ) )
61 60 rexbidv 
 |-  ( u = <. x , y >. -> ( E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = u /\ ( f ` 1 ) = <. z , w >. ) <-> E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = <. x , y >. /\ ( f ` 1 ) = <. z , w >. ) ) )
62 61 2ralbidv 
 |-  ( u = <. x , y >. -> ( A. z e. U. R A. w e. U. S E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = u /\ ( f ` 1 ) = <. z , w >. ) <-> A. z e. U. R A. w e. U. S E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = <. x , y >. /\ ( f ` 1 ) = <. z , w >. ) ) )
63 58 62 syl5bb 
 |-  ( u = <. x , y >. -> ( A. v e. ( U. R X. U. S ) E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = u /\ ( f ` 1 ) = v ) <-> A. z e. U. R A. w e. U. S E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = <. x , y >. /\ ( f ` 1 ) = <. z , w >. ) ) )
64 63 ralxp 
 |-  ( A. u e. ( U. R X. U. S ) A. v e. ( U. R X. U. S ) E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = u /\ ( f ` 1 ) = v ) <-> A. x e. U. R A. y e. U. S A. z e. U. R A. w e. U. S E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = <. x , y >. /\ ( f ` 1 ) = <. z , w >. ) )
65 54 64 sylibr 
 |-  ( ( R e. PConn /\ S e. PConn ) -> A. u e. ( U. R X. U. S ) A. v e. ( U. R X. U. S ) E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = u /\ ( f ` 1 ) = v ) )
66 6 8 txuni 
 |-  ( ( R e. Top /\ S e. Top ) -> ( U. R X. U. S ) = U. ( R tX S ) )
67 1 2 66 syl2an 
 |-  ( ( R e. PConn /\ S e. PConn ) -> ( U. R X. U. S ) = U. ( R tX S ) )
68 67 raleqdv 
 |-  ( ( R e. PConn /\ S e. PConn ) -> ( A. v e. ( U. R X. U. S ) E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = u /\ ( f ` 1 ) = v ) <-> A. v e. U. ( R tX S ) E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = u /\ ( f ` 1 ) = v ) ) )
69 67 68 raleqbidv 
 |-  ( ( R e. PConn /\ S e. PConn ) -> ( A. u e. ( U. R X. U. S ) A. v e. ( U. R X. U. S ) E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = u /\ ( f ` 1 ) = v ) <-> A. u e. U. ( R tX S ) A. v e. U. ( R tX S ) E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = u /\ ( f ` 1 ) = v ) ) )
70 65 69 mpbid 
 |-  ( ( R e. PConn /\ S e. PConn ) -> A. u e. U. ( R tX S ) A. v e. U. ( R tX S ) E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = u /\ ( f ` 1 ) = v ) )
71 eqid 
 |-  U. ( R tX S ) = U. ( R tX S )
72 71 ispconn 
 |-  ( ( R tX S ) e. PConn <-> ( ( R tX S ) e. Top /\ A. u e. U. ( R tX S ) A. v e. U. ( R tX S ) E. f e. ( II Cn ( R tX S ) ) ( ( f ` 0 ) = u /\ ( f ` 1 ) = v ) ) )
73 4 70 72 sylanbrc 
 |-  ( ( R e. PConn /\ S e. PConn ) -> ( R tX S ) e. PConn )