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) Remove dependency on ax-reg and ax-inf2 . (Revised by Timothy J. O'Malley, 15-Oct-2026)

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 fvex 
 |-  ( _I ` A ) e. _V
8 ovex 
 |-  ( II Cn ( F ` i ) ) e. _V
9 7 8 iunex 
 |-  U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) e. _V
10 fvi 
 |-  ( A e. V -> ( _I ` A ) = A )
11 10 ad2antrr 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> ( _I ` A ) = A )
12 11 eleq2d 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> ( t e. ( _I ` A ) <-> t e. A ) )
13 simplr 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> F : A --> PConn )
14 13 ffvelcdmda 
 |-  ( ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ t e. A ) -> ( F ` t ) e. PConn )
15 simprl 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> x e. U. ( Xt_ ` F ) )
16 eqid 
 |-  ( Xt_ ` F ) = ( Xt_ ` F )
17 16 ptuni 
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ t e. A U. ( F ` t ) = U. ( Xt_ ` F ) )
18 4 17 sylan2 
 |-  ( ( A e. V /\ F : A --> PConn ) -> X_ t e. A U. ( F ` t ) = U. ( Xt_ ` F ) )
19 18 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 ) )
20 15 19 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 ) )
21 vex 
 |-  x e. _V
22 21 elixp 
 |-  ( x e. X_ t e. A U. ( F ` t ) <-> ( x Fn A /\ A. t e. A ( x ` t ) e. U. ( F ` t ) ) )
23 20 22 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 ) ) )
24 23 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 ) )
25 24 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 ) )
26 simprr 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> y e. U. ( Xt_ ` F ) )
27 26 19 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 ) )
28 vex 
 |-  y e. _V
29 28 elixp 
 |-  ( y e. X_ t e. A U. ( F ` t ) <-> ( y Fn A /\ A. t e. A ( y ` t ) e. U. ( F ` t ) ) )
30 27 29 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 ) ) )
31 30 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 ) )
32 31 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 ) )
33 eqid 
 |-  U. ( F ` t ) = U. ( F ` t )
34 33 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 ) ) )
35 14 25 32 34 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 ) ) )
36 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 ) ) ) )
37 35 36 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 ) ) ) )
38 12 37 sylbida 
 |-  ( ( ( ( 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 ) ) ) )
39 38 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 ) ) ) )
40 fveq2 
 |-  ( i = t -> ( F ` i ) = ( F ` t ) )
41 40 oveq2d 
 |-  ( i = t -> ( II Cn ( F ` i ) ) = ( II Cn ( F ` t ) ) )
42 41 ssiun2s 
 |-  ( t e. ( _I ` A ) -> ( II Cn ( F ` t ) ) C_ U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) )
43 42 sseld 
 |-  ( t e. ( _I ` A ) -> ( f e. ( II Cn ( F ` t ) ) -> f e. U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) ) )
44 43 adantrd 
 |-  ( t e. ( _I ` A ) -> ( ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) -> f e. U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) ) )
45 44 ancrd 
 |-  ( t e. ( _I ` A ) -> ( ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) -> ( f e. U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) /\ ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) ) ) )
46 45 eximdv 
 |-  ( t e. ( _I ` A ) -> ( E. f ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) -> E. f ( f e. U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) /\ ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) ) ) )
47 df-rex 
 |-  ( E. f e. U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) <-> E. f ( f e. U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) /\ ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) ) )
48 46 47 imbitrrdi 
 |-  ( t e. ( _I ` A ) -> ( E. f ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) -> E. f e. U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) ) )
49 48 ralimia 
 |-  ( A. t e. ( _I ` A ) E. f ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) -> A. t e. ( _I ` A ) E. f e. U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) )
50 39 49 syl 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> A. t e. ( _I ` A ) E. f e. U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) )
51 eleq1 
 |-  ( f = ( g ` t ) -> ( f e. ( II Cn ( F ` t ) ) <-> ( g ` t ) e. ( II Cn ( F ` t ) ) ) )
52 fveq1 
 |-  ( f = ( g ` t ) -> ( f ` 0 ) = ( ( g ` t ) ` 0 ) )
53 52 eqeq1d 
 |-  ( f = ( g ` t ) -> ( ( f ` 0 ) = ( x ` t ) <-> ( ( g ` t ) ` 0 ) = ( x ` t ) ) )
54 fveq1 
 |-  ( f = ( g ` t ) -> ( f ` 1 ) = ( ( g ` t ) ` 1 ) )
55 54 eqeq1d 
 |-  ( f = ( g ` t ) -> ( ( f ` 1 ) = ( y ` t ) <-> ( ( g ` t ) ` 1 ) = ( y ` t ) ) )
56 53 55 anbi12d 
 |-  ( f = ( g ` t ) -> ( ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) <-> ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) )
57 51 56 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 ) ) ) ) )
58 57 ac6 
 |-  ( ( ( _I ` A ) e. _V /\ U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) e. _V /\ A. t e. ( _I ` A ) E. f e. U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) ( f e. ( II Cn ( F ` t ) ) /\ ( ( f ` 0 ) = ( x ` t ) /\ ( f ` 1 ) = ( y ` t ) ) ) ) -> E. g ( g : ( _I ` A ) --> U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) )
59 7 9 50 58 mp3an12i 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> E. g ( g : ( _I ` A ) --> U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) )
60 ffn 
 |-  ( g : ( _I ` A ) --> U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) -> g Fn ( _I ` A ) )
61 60 anim1i 
 |-  ( ( g : ( _I ` A ) --> U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) ) ) -> ( 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 ) ) ) ) )
62 61 eximi 
 |-  ( E. g ( g : ( _I ` A ) --> U_ i e. ( _I ` A ) ( II Cn ( F ` i ) ) /\ A. t e. ( _I ` A ) ( ( g ` t ) e. ( II Cn ( F ` t ) ) /\ ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 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 ) ) ) ) )
63 59 62 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 ) ) ) ) )
64 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
65 64 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 ) ) )
66 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 )
67 13 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 )
68 67 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 )
69 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 ) ) ) )
70 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 ) ) ) ) ) -> ( _I ` A ) = A )
71 70 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 ) )
72 71 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 ) )
73 fveq2 
 |-  ( t = i -> ( g ` t ) = ( g ` i ) )
74 fveq2 
 |-  ( t = i -> ( F ` t ) = ( F ` i ) )
75 74 oveq2d 
 |-  ( t = i -> ( II Cn ( F ` t ) ) = ( II Cn ( F ` i ) ) )
76 73 75 eleq12d 
 |-  ( t = i -> ( ( g ` t ) e. ( II Cn ( F ` t ) ) <-> ( g ` i ) e. ( II Cn ( F ` i ) ) ) )
77 73 fveq1d 
 |-  ( t = i -> ( ( g ` t ) ` 0 ) = ( ( g ` i ) ` 0 ) )
78 fveq2 
 |-  ( t = i -> ( x ` t ) = ( x ` i ) )
79 77 78 eqeq12d 
 |-  ( t = i -> ( ( ( g ` t ) ` 0 ) = ( x ` t ) <-> ( ( g ` i ) ` 0 ) = ( x ` i ) ) )
80 73 fveq1d 
 |-  ( t = i -> ( ( g ` t ) ` 1 ) = ( ( g ` i ) ` 1 ) )
81 fveq2 
 |-  ( t = i -> ( y ` t ) = ( y ` i ) )
82 80 81 eqeq12d 
 |-  ( t = i -> ( ( ( g ` t ) ` 1 ) = ( y ` t ) <-> ( ( g ` i ) ` 1 ) = ( y ` i ) ) )
83 79 82 anbi12d 
 |-  ( t = i -> ( ( ( ( g ` t ) ` 0 ) = ( x ` t ) /\ ( ( g ` t ) ` 1 ) = ( y ` t ) ) <-> ( ( ( g ` i ) ` 0 ) = ( x ` i ) /\ ( ( g ` i ) ` 1 ) = ( y ` i ) ) ) )
84 76 83 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 ) ) ) ) )
85 84 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 ) ) ) )
86 69 72 85 syl2an2r 
 |-  ( ( ( ( ( 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 ) ) ) )
87 86 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 ) ) )
88 iiuni 
 |-  ( 0 [,] 1 ) = U. II
89 eqid 
 |-  U. ( F ` i ) = U. ( F ` i )
90 88 89 cnf 
 |-  ( ( g ` i ) e. ( II Cn ( F ` i ) ) -> ( g ` i ) : ( 0 [,] 1 ) --> U. ( F ` i ) )
91 87 90 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 ) )
92 91 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 ) ) )
93 92 87 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 ) ) )
94 16 65 66 68 93 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 ) ) )
95 86 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 ) ) )
96 95 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 ) )
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 ) ` 0 ) ) = ( i e. A |-> ( x ` i ) ) )
98 0elunit 
 |-  0 e. ( 0 [,] 1 )
99 66 mptexd 
 |-  ( ( ( ( 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 )
100 fveq2 
 |-  ( z = 0 -> ( ( g ` i ) ` z ) = ( ( g ` i ) ` 0 ) )
101 100 mpteq2dv 
 |-  ( z = 0 -> ( i e. A |-> ( ( g ` i ) ` z ) ) = ( i e. A |-> ( ( g ` i ) ` 0 ) ) )
102 eqid 
 |-  ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) ) = ( z e. ( 0 [,] 1 ) |-> ( i e. A |-> ( ( g ` i ) ` z ) ) )
103 101 102 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 ) ) )
104 98 99 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 ) ) ) ` 0 ) = ( i e. A |-> ( ( g ` i ) ` 0 ) ) )
105 23 simpld 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> x 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 ) ) ) ) ) -> x Fn A )
107 dffn5 
 |-  ( x Fn A <-> x = ( i e. A |-> ( x ` 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 ) ) ) ) ) -> x = ( i e. A |-> ( x ` 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 ) ) ) ` 0 ) = x )
110 95 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 ) )
111 110 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 ) ) )
112 1elunit 
 |-  1 e. ( 0 [,] 1 )
113 66 mptexd 
 |-  ( ( ( ( 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 )
114 fveq2 
 |-  ( z = 1 -> ( ( g ` i ) ` z ) = ( ( g ` i ) ` 1 ) )
115 114 mpteq2dv 
 |-  ( z = 1 -> ( i e. A |-> ( ( g ` i ) ` z ) ) = ( i e. A |-> ( ( g ` i ) ` 1 ) ) )
116 115 102 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 ) ) )
117 112 113 116 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 ) ) )
118 30 simpld 
 |-  ( ( ( A e. V /\ F : A --> PConn ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> y Fn A )
119 118 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 )
120 dffn5 
 |-  ( y Fn A <-> y = ( i e. A |-> ( y ` i ) ) )
121 119 120 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 ) ) )
122 111 117 121 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 )
123 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 ) )
124 123 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 ) )
125 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 ) )
126 125 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 ) )
127 124 126 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 ) ) )
128 127 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 ) )
129 94 109 122 128 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 ) )
130 63 129 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 ) )
131 130 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 ) )
132 eqid 
 |-  U. ( Xt_ ` F ) = U. ( Xt_ ` F )
133 132 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 ) ) )
134 6 131 133 sylanbrc 
 |-  ( ( A e. V /\ F : A --> PConn ) -> ( Xt_ ` F ) e. PConn )