Metamath Proof Explorer

Theorem ptpconn

Description: The topological product of a collection of path-connected spaces is path-connected. The proof uses the axiom of choice. (Contributed by Mario Carneiro, 17-Feb-2015)

Ref Expression
Assertion ptpconn 
|- ( ( A e. V /\ F : A --> PConn ) -> ( Xt_ ` F ) e. PConn )

Proof

Step Hyp Ref Expression
1 pconntop 
 |-  ( x e. PConn -> x e. Top )
2 1 ssriv 
 |-  PConn C_ Top
3 fss 
 |-  ( ( F : A --> PConn /\ PConn C_ Top ) -> F : A --> Top )
4 2 3 mpan2 
 |-  ( F : A --> PConn -> F : A --> Top )
5 pttop 
 |-  ( ( A e. V /\ F : A --> Top ) -> ( Xt_ ` F ) e. Top )
6 4 5 sylan2 
 |-  ( ( A e. V /\ F : A --> PConn ) -> ( Xt_ ` F ) e. Top )
7 fvi 
 |-  ( A e. V -> ( _I ` A ) = A )
8 7 ad2antrr 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> ( _I ` A ) = A )
9 8 eleq2d 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> ( t e. ( _I ` A ) <-> t e. A ) )
10 9 biimpa 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ t e. ( _I ` A ) ) -> t e. A )
11 simplr 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> F : A --> PConn )
12 11 ffvelcdmda 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ t e. A ) -> ( F ` t ) e. PConn )
13 simprl 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> x e. U. ( Xt_ ` F ) )
14 eqid 
 |-  ( Xt_ ` F ) = ( Xt_ ` F )
15 14 ptuni 
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ t e. A U. ( F ` t ) = U. ( Xt_ ` F ) )
16 4 15 sylan2 
 |-  ( ( A e. V /\ F : A --> PConn ) -> X_ t e. A U. ( F ` t ) = U. ( Xt_ ` F ) )
17 16 adantr 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> X_ t e. A U. ( F ` t ) = U. ( Xt_ ` F ) )
18 13 17 eleqtrrd 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> x e. X_ t e. A U. ( F ` t ) )
19 vex 
 |-  x e. _V
20 19 elixp 
 |-  ( x e. X_ t e. A U. ( F ` t ) <-> ( x Fn A /\ A. t e. A ( x ` t ) e. U. ( F ` t ) ) )
21 18 20 sylib 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> ( x Fn A /\ A. t e. A ( x ` t ) e. U. ( F ` t ) ) )
22 21 simprd 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> A. t e. A ( x ` t ) e. U. ( F ` t ) )
23 22 r19.21bi 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ t e. A ) -> ( x ` t ) e. U. ( F ` t ) )
24 simprr 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> y e. U. ( Xt_ ` F ) )
25 24 17 eleqtrrd 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> y e. X_ t e. A U. ( F ` t ) )
26 vex 
 |-  y e. _V
27 26 elixp 
 |-  ( y e. X_ t e. A U. ( F ` t ) <-> ( y Fn A /\ A. t e. A ( y ` t ) e. U. ( F ` t ) ) )
28 25 27 sylib 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> ( y Fn A /\ A. t e. A ( y ` t ) e. U. ( F ` t ) ) )
29 28 simprd 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> A. t e. A ( y ` t ) e. U. ( F ` t ) )
30 29 r19.21bi 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ t e. A ) -> ( y ` t ) e. U. ( F ` t ) )
31 eqid 
 |-  U. ( F ` t ) = U. ( F ` t )
32 31 pconncn 
 |-  ( ( ( F ` t ) e. PConn /\ ( x ` t ) e. U. ( F ` t ) /\ ( y ` t ) e. U. ( F ` t ) ) -> E. f e. ( II Cn ( F ` t ) ) ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) )
33 12 23 30 32 syl3anc 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ t e. A ) -> E. f e. ( II Cn ( F ` t ) ) ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) )
34 df-rex 
 |-  ( E. f e. ( II Cn ( F ` t ) ) ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) <-> E. f ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) )
35 33 34 sylib 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ t e. A ) -> E. f ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) )
36 10 35 syldan 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ t e. ( _I ` A ) ) -> E. f ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) )
37 36 ralrimiva 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> A. t e. ( _I ` A ) E. f ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) )
38 fvex 
 |-  ( _I ` A ) e. _V
39 eleq1 
 |-  ( f = ( g ` t ) -> ( f e. ( II Cn ( F ` t ) ) <-> ( g ` t ) e. ( II Cn ( F ` t ) ) ) )
40 fveq1 
 |-  ( f = ( g ` t ) -> ( f ` 0 ) = ( ( g ` t ) ` 0 ) )
41 40 eqeq1d 
 |-  ( f = ( g ` t ) -> ( ( f ` 0 ) = ( x ` t ) <-> ( ( g ` t ) ` 0 ) = ( x ` t ) ) )
42 fveq1 
 |-  ( f = ( g ` t ) -> ( f ` 1 ) = ( ( g ` t ) ` 1 ) )
43 42 eqeq1d 
 |-  ( f = ( g ` t ) -> ( ( f ` 1 ) = ( y ` t ) <-> ( ( g ` t ) ` 1 ) = ( y ` t ) ) )
44 41 43 anbi12d 
 |-  ( f = ( g ` t ) -> ( ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) <-> ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) )
45 39 44 anbi12d 
 |-  ( f = ( g ` t ) -> ( ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) <-> ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) )
46 38 45 ac6s2 
 |-  ( A. t e. ( _I ` A ) E. f ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) -> E. g ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) )
47 37 46 syl 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> E. g ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) )
48 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
49 48 a1i 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
50 simplll 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> A e. V )
51 11 adantr 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> F : A --> PConn )
52 51 4 syl 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> F : A --> Top )
53 8 adantr 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> ( _I ` A ) = A )
54 53 eleq2d 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> ( i e. ( _I ` A ) <-> i e. A ) )
55 54 biimpar 
 |-  ( ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) /\ i e. A ) -> i e. ( _I ` A ) )
56 simprr 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) )
57 fveq2 
 |-  ( t = i -> ( g ` t ) = ( g ` i ) )
58 fveq2 
 |-  ( t = i -> ( F ` t ) = ( F ` i ) )
59 58 oveq2d 
 |-  ( t = i -> ( II Cn ( F ` t ) ) = ( II Cn ( F ` i ) ) )
60 57 59 eleq12d 
 |-  ( t = i -> ( ( g ` t ) e. ( II Cn ( F ` t ) ) <-> ( g ` i ) e. ( II Cn ( F ` i ) ) ) )
61 57 fveq1d 
 |-  ( t = i -> ( ( g ` t ) ` 0 ) = ( ( g ` i ) ` 0 ) )
62 fveq2 
 |-  ( t = i -> ( x ` t ) = ( x ` i ) )
63 61 62 eqeq12d 
 |-  ( t = i -> ( ( ( g ` t ) ` 0 ) = ( x ` t ) <-> ( ( g ` i ) ` 0 ) = ( x ` i ) ) )
64 57 fveq1d 
 |-  ( t = i -> ( ( g ` t ) ` 1 ) = ( ( g ` i ) ` 1 ) )
65 fveq2 
 |-  ( t = i -> ( y ` t ) = ( y ` i ) )
66 64 65 eqeq12d 
 |-  ( t = i -> ( ( ( g ` t ) ` 1 ) = ( y ` t ) <-> ( ( g ` i ) ` 1 ) = ( y ` i ) ) )
67 63 66 anbi12d 
 |-  ( t = i -> ( ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) <-> ( ( ( g ` i ) ` 0 ) = ( x ` i ) /\ ( ( g ` i ) ` 1 ) = ( y ` i ) ) ) )
68 60 67 anbi12d 
 |-  ( t = i -> ( ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) <-> ( ( g ` i ) e. ( II Cn ( F ` i ) ) /\ ( ( ( g ` i ) ` 0 ) = ( x ` i ) /\ ( ( g ` i ) ` 1 ) = ( y ` i ) ) ) ) )
69 68 rspccva 
 |-  ( ( A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) /\ i e. ( _I ` A ) ) -> ( ( g ` i ) e. ( II Cn ( F ` i ) ) /\ ( ( ( g ` i ) ` 0 ) = ( x ` i ) /\ ( ( g ` i ) ` 1 ) = ( y ` i ) ) ) )
70 56 69 sylan 
 |-  ( ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) /\ i e. ( _I ` A ) ) -> ( ( g ` i ) e. ( II Cn ( F ` i ) ) /\ ( ( ( g ` i ) ` 0 ) = ( x ` i ) /\ ( ( g ` i ) ` 1 ) = ( y ` i ) ) ) )
71 55 70 syldan 
 |-  ( ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) /\ i e. A ) -> ( ( g ` i ) e. ( II Cn ( F ` i ) ) /\ ( ( ( g ` i ) ` 0 ) = ( x ` i ) /\ ( ( g ` i ) ` 1 ) = ( y ` i ) ) ) )
72 71 simpld 
 |-  ( ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) /\ i e. A ) -> ( g ` i ) e. ( II Cn ( F ` i ) ) )
73 iiuni 
 |-  ( 0 [,] 1 ) = U. II
74 eqid 
 |-  U. ( F ` i ) = U. ( F ` i )
75 73 74 cnf 
 |-  ( ( g ` i ) e. ( II Cn ( F ` i ) ) -> ( g ` i ) : ( 0 [,] 1 ) --> U. ( F ` i ) )
76 72 75 syl 
 |-  ( ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) /\ i e. A ) -> ( g ` i ) : ( 0 [,] 1 ) --> U. ( F ` i ) )
77 76 feqmptd 
 |-  ( ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) /\ i e. A ) -> ( g ` i ) = ( z e. ( 0 [,] 1 ) |-> ( ( g ` i ) ` z ) ) )
78 77 72 eqeltrrd 
 |-  ( ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) /\ i e. A ) -> ( z e. ( 0 [,] 1 ) |-> ( ( g ` i ) ` z ) ) e. ( II Cn ( F ` i ) ) )
79 14 49 50 52 78 ptcn 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) e. ( II Cn ( Xt_ ` F ) ) )
80 71 simprd 
 |-  ( ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) /\ i e. A ) -> ( ( ( g ` i ) ` 0 ) = ( x ` i ) /\ ( ( g ` i ) ` 1 ) = ( y ` i ) ) )
81 80 simpld 
 |-  ( ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) /\ i e. A ) -> ( ( g ` i ) ` 0 ) = ( x ` i ) )
82 81 mpteq2dva 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> ( i e. A |-> ( ( g ` i ) ` 0 ) ) = ( i e. A |-> ( x ` i ) ) )
83 0elunit 
 |-  0 e. ( 0 [,] 1 )
84 mptexg 
 |-  ( A e. V -> ( i e. A |-> ( ( g ` i ) ` 0 ) ) e. _V )
85 50 84 syl 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> ( i e. A |-> ( ( g ` i ) ` 0 ) ) e. _V )
86 fveq2 
 |-  ( z = 0 -> ( ( g ` i ) ` z ) = ( ( g ` i ) ` 0 ) )
87 86 mpteq2dv 
 |-  ( z = 0 -> ( i e. A |-> ( ( g ` i ) ` z ) ) = ( i e. A |-> ( ( g ` i ) ` 0 ) ) )
88 eqid 
 |-  ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) = ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) )
89 87 88 fvmptg 
 |-  ( ( 0 e. ( 0 [,] 1 ) /\ ( i e. A |-> ( ( g ` i ) ` 0 ) ) e. _V ) -> ( ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) ` 0 ) = ( i e. A |-> ( ( g ` i ) ` 0 ) ) )
90 83 85 89 sylancr 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> ( ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) ` 0 ) = ( i e. A |-> ( ( g ` i ) ` 0 ) ) )
91 21 simpld 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> x Fn A )
92 91 adantr 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> x Fn A )
93 dffn5 
 |-  ( x Fn A <-> x = ( i e. A |-> ( x ` i ) ) )
94 92 93 sylib 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> x = ( i e. A |-> ( x ` i ) ) )
95 82 90 94 3eqtr4d 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> ( ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) ` 0 ) = x )
96 80 simprd 
 |-  ( ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) /\ i e. A ) -> ( ( g ` i ) ` 1 ) = ( y ` i ) )
97 96 mpteq2dva 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> ( i e. A |-> ( ( g ` i ) ` 1 ) ) = ( i e. A |-> ( y ` i ) ) )
98 1elunit 
 |-  1 e. ( 0 [,] 1 )
99 mptexg 
 |-  ( A e. V -> ( i e. A |-> ( ( g ` i ) ` 1 ) ) e. _V )
100 50 99 syl 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> ( i e. A |-> ( ( g ` i ) ` 1 ) ) e. _V )
101 fveq2 
 |-  ( z = 1 -> ( ( g ` i ) ` z ) = ( ( g ` i ) ` 1 ) )
102 101 mpteq2dv 
 |-  ( z = 1 -> ( i e. A |-> ( ( g ` i ) ` z ) ) = ( i e. A |-> ( ( g ` i ) ` 1 ) ) )
103 102 88 fvmptg 
 |-  ( ( 1 e. ( 0 [,] 1 ) /\ ( i e. A |-> ( ( g ` i ) ` 1 ) ) e. _V ) -> ( ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) ` 1 ) = ( i e. A |-> ( ( g ` i ) ` 1 ) ) )
104 98 100 103 sylancr 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> ( ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) ` 1 ) = ( i e. A |-> ( ( g ` i ) ` 1 ) ) )
105 28 simpld 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> y Fn A )
106 105 adantr 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> y Fn A )
107 dffn5 
 |-  ( y Fn A <-> y = ( i e. A |-> ( y ` i ) ) )
108 106 107 sylib 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> y = ( i e. A |-> ( y ` i ) ) )
109 97 104 108 3eqtr4d 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> ( ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) ` 1 ) = y )
110 fveq1 
 |-  ( f = ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) -> ( f ` 0 ) = ( ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) ` 0 ) )
111 110 eqeq1d 
 |-  ( f = ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) -> ( ( f ` 0 ) = x <-> ( ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) ` 0 ) = x ) )
112 fveq1 
 |-  ( f = ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) -> ( f ` 1 ) = ( ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) ` 1 ) )
113 112 eqeq1d 
 |-  ( f = ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) -> ( ( f ` 1 ) = y <-> ( ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) ` 1 ) = y ) )
114 111 113 anbi12d 
 |-  ( f = ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) -> ( ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) <-> ( ( ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) ` 0 ) = x /\ ( ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) ` 1 ) = y ) ) )
115 114 rspcev 
 |-  ( ( ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) e. ( II Cn ( Xt_ ` F ) ) /\ ( ( ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) ` 0 ) = x /\ ( ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) ` 1 ) = y ) ) -> E. f e. ( II Cn ( Xt_ ` F ) ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
116 79 95 109 115 syl12anc 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( g Fn ( _I ` A ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) ) -> E. f e. ( II Cn ( Xt_ ` F ) ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
117 47 116 exlimddv 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> E. f e. ( II Cn ( Xt_ ` F ) ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
118 117 ralrimivva 
 |-  ( ( A e. V /\ F : A --> PConn ) -> A. x e. U. ( Xt_ ` F ) A. y e. U. ( Xt_ ` F ) E. f e. ( II Cn ( Xt_ ` F ) ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
119 eqid 
 |-  U. ( Xt_ ` F ) = U. ( Xt_ ` F )
120 119 ispconn 
 |-  ( ( Xt_ ` F ) e. PConn <-> ( ( Xt_ ` F ) e. Top /\ A. x e. U. ( Xt_ ` F ) A. y e. U. ( Xt_ ` F ) E. f e. ( II Cn ( Xt_ ` F ) ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) ) )
121 6 118 120 sylanbrc 
 |-  ( ( A e. V /\ F : A --> PConn ) -> ( Xt_ ` F ) e. PConn )