Metamath Proof Explorer

Theorem poimirlem30

Description: Lemma for poimir combining poimirlem29 with bwth . (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 
|- ( ph -> N e. NN )
poimir.i 
|- I = ( ( 0 [,] 1 ) ^m ( 1 ... N ) )
poimir.r 
|- R = ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) )
poimir.1 
|- ( ph -> F e. ( ( R |`t I ) Cn R ) )
poimirlem30.x 
|- X = ( ( F ` ( ( ( 1st ` ( G ` k ) ) oF + ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` n )
poimirlem30.2 
|- ( ph -> G : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
poimirlem30.3 
|- ( ( ph /\ k e. NN ) -> ran ( 1st ` ( G ` k ) ) C_ ( 0 ..^ k ) )
poimirlem30.4 
|- ( ( ph /\ ( k e. NN /\ n e. ( 1 ... N ) /\ r e. { <_ , `' <_ } ) ) -> E. j e. ( 0 ... N ) 0 r X )
Assertion poimirlem30 
|- ( ph -> E. c e. I A. n e. ( 1 ... N ) A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )

Proof

Step Hyp Ref Expression
1 poimir.0 
 |-  ( ph -> N e. NN )
2 poimir.i 
 |-  I = ( ( 0 [,] 1 ) ^m ( 1 ... N ) )
3 poimir.r 
 |-  R = ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) )
4 poimir.1 
 |-  ( ph -> F e. ( ( R |`t I ) Cn R ) )
5 poimirlem30.x 
 |-  X = ( ( F ` ( ( ( 1st ` ( G ` k ) ) oF + ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` n )
6 poimirlem30.2 
 |-  ( ph -> G : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
7 poimirlem30.3 
 |-  ( ( ph /\ k e. NN ) -> ran ( 1st ` ( G ` k ) ) C_ ( 0 ..^ k ) )
8 poimirlem30.4 
 |-  ( ( ph /\ ( k e. NN /\ n e. ( 1 ... N ) /\ r e. { <_ , `' <_ } ) ) -> E. j e. ( 0 ... N ) 0 r X )
9 elfzonn0 
 |-  ( i e. ( 0 ..^ k ) -> i e. NN0 )
10 9 nn0red 
 |-  ( i e. ( 0 ..^ k ) -> i e. RR )
11 nndivre 
 |-  ( ( i e. RR /\ k e. NN ) -> ( i / k ) e. RR )
12 10 11 sylan 
 |-  ( ( i e. ( 0 ..^ k ) /\ k e. NN ) -> ( i / k ) e. RR )
13 elfzole1 
 |-  ( i e. ( 0 ..^ k ) -> 0 <_ i )
14 10 13 jca 
 |-  ( i e. ( 0 ..^ k ) -> ( i e. RR /\ 0 <_ i ) )
15 nnrp 
 |-  ( k e. NN -> k e. RR+ )
16 15 rpregt0d 
 |-  ( k e. NN -> ( k e. RR /\ 0 < k ) )
17 divge0 
 |-  ( ( ( i e. RR /\ 0 <_ i ) /\ ( k e. RR /\ 0 < k ) ) -> 0 <_ ( i / k ) )
18 14 16 17 syl2an 
 |-  ( ( i e. ( 0 ..^ k ) /\ k e. NN ) -> 0 <_ ( i / k ) )
19 elfzo0le 
 |-  ( i e. ( 0 ..^ k ) -> i <_ k )
20 19 adantr 
 |-  ( ( i e. ( 0 ..^ k ) /\ k e. NN ) -> i <_ k )
21 10 adantr 
 |-  ( ( i e. ( 0 ..^ k ) /\ k e. NN ) -> i e. RR )
22 1red 
 |-  ( ( i e. ( 0 ..^ k ) /\ k e. NN ) -> 1 e. RR )
23 15 adantl 
 |-  ( ( i e. ( 0 ..^ k ) /\ k e. NN ) -> k e. RR+ )
24 21 22 23 ledivmuld 
 |-  ( ( i e. ( 0 ..^ k ) /\ k e. NN ) -> ( ( i / k ) <_ 1 <-> i <_ ( k x. 1 ) ) )
25 nncn 
 |-  ( k e. NN -> k e. CC )
26 25 mulridd 
 |-  ( k e. NN -> ( k x. 1 ) = k )
27 26 breq2d 
 |-  ( k e. NN -> ( i <_ ( k x. 1 ) <-> i <_ k ) )
28 27 adantl 
 |-  ( ( i e. ( 0 ..^ k ) /\ k e. NN ) -> ( i <_ ( k x. 1 ) <-> i <_ k ) )
29 24 28 bitrd 
 |-  ( ( i e. ( 0 ..^ k ) /\ k e. NN ) -> ( ( i / k ) <_ 1 <-> i <_ k ) )
30 20 29 mpbird 
 |-  ( ( i e. ( 0 ..^ k ) /\ k e. NN ) -> ( i / k ) <_ 1 )
31 elicc01 
 |-  ( ( i / k ) e. ( 0 [,] 1 ) <-> ( ( i / k ) e. RR /\ 0 <_ ( i / k ) /\ ( i / k ) <_ 1 ) )
32 12 18 30 31 syl3anbrc 
 |-  ( ( i e. ( 0 ..^ k ) /\ k e. NN ) -> ( i / k ) e. ( 0 [,] 1 ) )
33 32 ancoms 
 |-  ( ( k e. NN /\ i e. ( 0 ..^ k ) ) -> ( i / k ) e. ( 0 [,] 1 ) )
34 elsni 
 |-  ( j e. { k } -> j = k )
35 34 oveq2d 
 |-  ( j e. { k } -> ( i / j ) = ( i / k ) )
36 35 eleq1d 
 |-  ( j e. { k } -> ( ( i / j ) e. ( 0 [,] 1 ) <-> ( i / k ) e. ( 0 [,] 1 ) ) )
37 33 36 syl5ibrcom 
 |-  ( ( k e. NN /\ i e. ( 0 ..^ k ) ) -> ( j e. { k } -> ( i / j ) e. ( 0 [,] 1 ) ) )
38 37 impr 
 |-  ( ( k e. NN /\ ( i e. ( 0 ..^ k ) /\ j e. { k } ) ) -> ( i / j ) e. ( 0 [,] 1 ) )
39 38 adantll 
 |-  ( ( ( ph /\ k e. NN ) /\ ( i e. ( 0 ..^ k ) /\ j e. { k } ) ) -> ( i / j ) e. ( 0 [,] 1 ) )
40 6 ffvelcdmda 
 |-  ( ( ph /\ k e. NN ) -> ( G ` k ) e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
41 xp1st 
 |-  ( ( G ` k ) e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 1st ` ( G ` k ) ) e. ( NN0 ^m ( 1 ... N ) ) )
42 elmapfn 
 |-  ( ( 1st ` ( G ` k ) ) e. ( NN0 ^m ( 1 ... N ) ) -> ( 1st ` ( G ` k ) ) Fn ( 1 ... N ) )
43 40 41 42 3syl 
 |-  ( ( ph /\ k e. NN ) -> ( 1st ` ( G ` k ) ) Fn ( 1 ... N ) )
44 df-f 
 |-  ( ( 1st ` ( G ` k ) ) : ( 1 ... N ) --> ( 0 ..^ k ) <-> ( ( 1st ` ( G ` k ) ) Fn ( 1 ... N ) /\ ran ( 1st ` ( G ` k ) ) C_ ( 0 ..^ k ) ) )
45 43 7 44 sylanbrc 
 |-  ( ( ph /\ k e. NN ) -> ( 1st ` ( G ` k ) ) : ( 1 ... N ) --> ( 0 ..^ k ) )
46 vex 
 |-  k e. _V
47 46 fconst 
 |-  ( ( 1 ... N ) X. { k } ) : ( 1 ... N ) --> { k }
48 47 a1i 
 |-  ( ( ph /\ k e. NN ) -> ( ( 1 ... N ) X. { k } ) : ( 1 ... N ) --> { k } )
49 fzfid 
 |-  ( ( ph /\ k e. NN ) -> ( 1 ... N ) e. Fin )
50 inidm 
 |-  ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
51 39 45 48 49 49 50 off 
 |-  ( ( ph /\ k e. NN ) -> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
52 2 eleq2i 
 |-  ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) e. I <-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) )
53 ovex 
 |-  ( 0 [,] 1 ) e. _V
54 ovex 
 |-  ( 1 ... N ) e. _V
55 53 54 elmap 
 |-  ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) <-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
56 52 55 bitri 
 |-  ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) e. I <-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
57 51 56 sylibr 
 |-  ( ( ph /\ k e. NN ) -> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) e. I )
58 57 fmpttd 
 |-  ( ph -> ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) : NN --> I )
59 58 frnd 
 |-  ( ph -> ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) C_ I )
60 ominf 
 |-  -. _om e. Fin
61 nnenom 
 |-  NN ~~ _om
62 enfi 
 |-  ( NN ~~ _om -> ( NN e. Fin <-> _om e. Fin ) )
63 61 62 ax-mp 
 |-  ( NN e. Fin <-> _om e. Fin )
64 iunid 
 |-  U_ c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) { c } = ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) )
65 64 imaeq2i 
 |-  ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " U_ c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) { c } ) = ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) )
66 imaiun 
 |-  ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " U_ c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) { c } ) = U_ c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } )
67 ovex 
 |-  ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) e. _V
68 eqid 
 |-  ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) = ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) )
69 67 68 fnmpti 
 |-  ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) Fn NN
70 dffn3 
 |-  ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) Fn NN <-> ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) : NN --> ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) )
71 69 70 mpbi 
 |-  ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) : NN --> ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) )
72 fimacnv 
 |-  ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) : NN --> ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) -> ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) = NN )
73 71 72 ax-mp 
 |-  ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) = NN
74 65 66 73 3eqtr3ri 
 |-  NN = U_ c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } )
75 74 eleq1i 
 |-  ( NN e. Fin <-> U_ c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) e. Fin )
76 63 75 bitr3i 
 |-  ( _om e. Fin <-> U_ c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) e. Fin )
77 60 76 mtbi 
 |-  -. U_ c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) e. Fin
78 ralnex 
 |-  ( A. k e. ( ZZ>= ` i ) -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c <-> -. E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c )
79 78 rexbii 
 |-  ( E. i e. NN A. k e. ( ZZ>= ` i ) -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c <-> E. i e. NN -. E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c )
80 rexnal 
 |-  ( E. i e. NN -. E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c <-> -. A. i e. NN E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c )
81 79 80 bitri 
 |-  ( E. i e. NN A. k e. ( ZZ>= ` i ) -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c <-> -. A. i e. NN E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c )
82 81 ralbii 
 |-  ( A. c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) E. i e. NN A. k e. ( ZZ>= ` i ) -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c <-> A. c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) -. A. i e. NN E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c )
83 ralnex 
 |-  ( A. c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) -. A. i e. NN E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c <-> -. E. c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) A. i e. NN E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c )
84 82 83 bitri 
 |-  ( A. c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) E. i e. NN A. k e. ( ZZ>= ` i ) -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c <-> -. E. c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) A. i e. NN E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c )
85 nnuz 
 |-  NN = ( ZZ>= ` 1 )
86 elnnuz 
 |-  ( i e. NN <-> i e. ( ZZ>= ` 1 ) )
87 fzouzsplit 
 |-  ( i e. ( ZZ>= ` 1 ) -> ( ZZ>= ` 1 ) = ( ( 1 ..^ i ) u. ( ZZ>= ` i ) ) )
88 86 87 sylbi 
 |-  ( i e. NN -> ( ZZ>= ` 1 ) = ( ( 1 ..^ i ) u. ( ZZ>= ` i ) ) )
89 85 88 eqtrid 
 |-  ( i e. NN -> NN = ( ( 1 ..^ i ) u. ( ZZ>= ` i ) ) )
90 89 difeq1d 
 |-  ( i e. NN -> ( NN \ ( 1 ..^ i ) ) = ( ( ( 1 ..^ i ) u. ( ZZ>= ` i ) ) \ ( 1 ..^ i ) ) )
91 uncom 
 |-  ( ( 1 ..^ i ) u. ( ZZ>= ` i ) ) = ( ( ZZ>= ` i ) u. ( 1 ..^ i ) )
92 91 difeq1i 
 |-  ( ( ( 1 ..^ i ) u. ( ZZ>= ` i ) ) \ ( 1 ..^ i ) ) = ( ( ( ZZ>= ` i ) u. ( 1 ..^ i ) ) \ ( 1 ..^ i ) )
93 difun2 
 |-  ( ( ( ZZ>= ` i ) u. ( 1 ..^ i ) ) \ ( 1 ..^ i ) ) = ( ( ZZ>= ` i ) \ ( 1 ..^ i ) )
94 92 93 eqtri 
 |-  ( ( ( 1 ..^ i ) u. ( ZZ>= ` i ) ) \ ( 1 ..^ i ) ) = ( ( ZZ>= ` i ) \ ( 1 ..^ i ) )
95 90 94 eqtrdi 
 |-  ( i e. NN -> ( NN \ ( 1 ..^ i ) ) = ( ( ZZ>= ` i ) \ ( 1 ..^ i ) ) )
96 difss 
 |-  ( ( ZZ>= ` i ) \ ( 1 ..^ i ) ) C_ ( ZZ>= ` i )
97 95 96 eqsstrdi 
 |-  ( i e. NN -> ( NN \ ( 1 ..^ i ) ) C_ ( ZZ>= ` i ) )
98 ssralv 
 |-  ( ( NN \ ( 1 ..^ i ) ) C_ ( ZZ>= ` i ) -> ( A. k e. ( ZZ>= ` i ) -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> A. k e. ( NN \ ( 1 ..^ i ) ) -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c ) )
99 97 98 syl 
 |-  ( i e. NN -> ( A. k e. ( ZZ>= ` i ) -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> A. k e. ( NN \ ( 1 ..^ i ) ) -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c ) )
100 impexp 
 |-  ( ( ( k e. NN /\ -. k e. ( 1 ..^ i ) ) -> -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c ) <-> ( k e. NN -> ( -. k e. ( 1 ..^ i ) -> -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c ) ) )
101 eldif 
 |-  ( k e. ( NN \ ( 1 ..^ i ) ) <-> ( k e. NN /\ -. k e. ( 1 ..^ i ) ) )
102 101 imbi1i 
 |-  ( ( k e. ( NN \ ( 1 ..^ i ) ) -> -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c ) <-> ( ( k e. NN /\ -. k e. ( 1 ..^ i ) ) -> -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c ) )
103 con34b 
 |-  ( ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> k e. ( 1 ..^ i ) ) <-> ( -. k e. ( 1 ..^ i ) -> -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c ) )
104 103 imbi2i 
 |-  ( ( k e. NN -> ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> k e. ( 1 ..^ i ) ) ) <-> ( k e. NN -> ( -. k e. ( 1 ..^ i ) -> -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c ) ) )
105 100 102 104 3bitr4i 
 |-  ( ( k e. ( NN \ ( 1 ..^ i ) ) -> -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c ) <-> ( k e. NN -> ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> k e. ( 1 ..^ i ) ) ) )
106 105 albii 
 |-  ( A. k ( k e. ( NN \ ( 1 ..^ i ) ) -> -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c ) <-> A. k ( k e. NN -> ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> k e. ( 1 ..^ i ) ) ) )
107 df-ral 
 |-  ( A. k e. ( NN \ ( 1 ..^ i ) ) -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c <-> A. k ( k e. ( NN \ ( 1 ..^ i ) ) -> -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c ) )
108 vex 
 |-  c e. _V
109 68 mptiniseg 
 |-  ( c e. _V -> ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) = { k e. NN | ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c } )
110 108 109 ax-mp 
 |-  ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) = { k e. NN | ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c }
111 110 sseq1i 
 |-  ( ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) C_ ( 1 ..^ i ) <-> { k e. NN | ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c } C_ ( 1 ..^ i ) )
112 rabss 
 |-  ( { k e. NN | ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c } C_ ( 1 ..^ i ) <-> A. k e. NN ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> k e. ( 1 ..^ i ) ) )
113 df-ral 
 |-  ( A. k e. NN ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> k e. ( 1 ..^ i ) ) <-> A. k ( k e. NN -> ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> k e. ( 1 ..^ i ) ) ) )
114 111 112 113 3bitri 
 |-  ( ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) C_ ( 1 ..^ i ) <-> A. k ( k e. NN -> ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> k e. ( 1 ..^ i ) ) ) )
115 106 107 114 3bitr4i 
 |-  ( A. k e. ( NN \ ( 1 ..^ i ) ) -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c <-> ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) C_ ( 1 ..^ i ) )
116 fzofi 
 |-  ( 1 ..^ i ) e. Fin
117 ssfi 
 |-  ( ( ( 1 ..^ i ) e. Fin /\ ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) C_ ( 1 ..^ i ) ) -> ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) e. Fin )
118 116 117 mpan 
 |-  ( ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) C_ ( 1 ..^ i ) -> ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) e. Fin )
119 115 118 sylbi 
 |-  ( A. k e. ( NN \ ( 1 ..^ i ) ) -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) e. Fin )
120 99 119 syl6 
 |-  ( i e. NN -> ( A. k e. ( ZZ>= ` i ) -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) e. Fin ) )
121 120 rexlimiv 
 |-  ( E. i e. NN A. k e. ( ZZ>= ` i ) -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) e. Fin )
122 121 ralimi 
 |-  ( A. c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) E. i e. NN A. k e. ( ZZ>= ` i ) -. ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> A. c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) e. Fin )
123 84 122 sylbir 
 |-  ( -. E. c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) A. i e. NN E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> A. c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) e. Fin )
124 iunfi 
 |-  ( ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) e. Fin /\ A. c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) e. Fin ) -> U_ c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) e. Fin )
125 124 ex 
 |-  ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) e. Fin -> ( A. c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) e. Fin -> U_ c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) e. Fin ) )
126 123 125 syl5 
 |-  ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) e. Fin -> ( -. E. c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) A. i e. NN E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> U_ c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ( `' ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " { c } ) e. Fin ) )
127 77 126 mt3i 
 |-  ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) e. Fin -> E. c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) A. i e. NN E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c )
128 ssrexv 
 |-  ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) C_ I -> ( E. c e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) A. i e. NN E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> E. c e. I A. i e. NN E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c ) )
129 59 127 128 syl2im 
 |-  ( ph -> ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) e. Fin -> E. c e. I A. i e. NN E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c ) )
130 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
131 elmapi 
 |-  ( c e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) -> c : ( 1 ... N ) --> ( 0 [,] 1 ) )
132 131 2 eleq2s 
 |-  ( c e. I -> c : ( 1 ... N ) --> ( 0 [,] 1 ) )
133 132 ffvelcdmda 
 |-  ( ( c e. I /\ m e. ( 1 ... N ) ) -> ( c ` m ) e. ( 0 [,] 1 ) )
134 130 133 sselid 
 |-  ( ( c e. I /\ m e. ( 1 ... N ) ) -> ( c ` m ) e. RR )
135 nnrp 
 |-  ( i e. NN -> i e. RR+ )
136 135 rpreccld 
 |-  ( i e. NN -> ( 1 / i ) e. RR+ )
137 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
138 137 rexmet 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )
139 blcntr 
 |-  ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) /\ ( c ` m ) e. RR /\ ( 1 / i ) e. RR+ ) -> ( c ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) )
140 138 139 mp3an1 
 |-  ( ( ( c ` m ) e. RR /\ ( 1 / i ) e. RR+ ) -> ( c ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) )
141 134 136 140 syl2an 
 |-  ( ( ( c e. I /\ m e. ( 1 ... N ) ) /\ i e. NN ) -> ( c ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) )
142 141 an32s 
 |-  ( ( ( c e. I /\ i e. NN ) /\ m e. ( 1 ... N ) ) -> ( c ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) )
143 fveq1 
 |-  ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) = ( c ` m ) )
144 143 eleq1d 
 |-  ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> ( ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) <-> ( c ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
145 142 144 syl5ibrcom 
 |-  ( ( ( c e. I /\ i e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
146 145 ralrimdva 
 |-  ( ( c e. I /\ i e. NN ) -> ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
147 146 reximdv 
 |-  ( ( c e. I /\ i e. NN ) -> ( E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
148 147 ralimdva 
 |-  ( c e. I -> ( A. i e. NN E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> A. i e. NN E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
149 148 reximia 
 |-  ( E. c e. I A. i e. NN E. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) = c -> E. c e. I A. i e. NN E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) )
150 129 149 syl6 
 |-  ( ph -> ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) e. Fin -> E. c e. I A. i e. NN E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
151 54 53 ixpconst 
 |-  X_ n e. ( 1 ... N ) ( 0 [,] 1 ) = ( ( 0 [,] 1 ) ^m ( 1 ... N ) )
152 2 151 eqtr4i 
 |-  I = X_ n e. ( 1 ... N ) ( 0 [,] 1 )
153 3 152 oveq12i 
 |-  ( R |`t I ) = ( ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ) |`t X_ n e. ( 1 ... N ) ( 0 [,] 1 ) )
154 fzfid 
 |-  ( T. -> ( 1 ... N ) e. Fin )
155 retop 
 |-  ( topGen ` ran (,) ) e. Top
156 155 fconst6 
 |-  ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) : ( 1 ... N ) --> Top
157 156 a1i 
 |-  ( T. -> ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) : ( 1 ... N ) --> Top )
158 53 a1i 
 |-  ( ( T. /\ n e. ( 1 ... N ) ) -> ( 0 [,] 1 ) e. _V )
159 154 157 158 ptrest 
 |-  ( T. -> ( ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ) |`t X_ n e. ( 1 ... N ) ( 0 [,] 1 ) ) = ( Xt_ ` ( n e. ( 1 ... N ) |-> ( ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) |`t ( 0 [,] 1 ) ) ) ) )
160 159 mptru 
 |-  ( ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ) |`t X_ n e. ( 1 ... N ) ( 0 [,] 1 ) ) = ( Xt_ ` ( n e. ( 1 ... N ) |-> ( ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) |`t ( 0 [,] 1 ) ) ) )
161 fvex 
 |-  ( topGen ` ran (,) ) e. _V
162 161 fvconst2 
 |-  ( n e. ( 1 ... N ) -> ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) = ( topGen ` ran (,) ) )
163 162 oveq1d 
 |-  ( n e. ( 1 ... N ) -> ( ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) |`t ( 0 [,] 1 ) ) = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) )
164 163 mpteq2ia 
 |-  ( n e. ( 1 ... N ) |-> ( ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) |`t ( 0 [,] 1 ) ) ) = ( n e. ( 1 ... N ) |-> ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) )
165 fconstmpt 
 |-  ( ( 1 ... N ) X. { ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) } ) = ( n e. ( 1 ... N ) |-> ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) )
166 164 165 eqtr4i 
 |-  ( n e. ( 1 ... N ) |-> ( ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) |`t ( 0 [,] 1 ) ) ) = ( ( 1 ... N ) X. { ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) } )
167 166 fveq2i 
 |-  ( Xt_ ` ( n e. ( 1 ... N ) |-> ( ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) |`t ( 0 [,] 1 ) ) ) ) = ( Xt_ ` ( ( 1 ... N ) X. { ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) } ) )
168 153 160 167 3eqtri 
 |-  ( R |`t I ) = ( Xt_ ` ( ( 1 ... N ) X. { ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) } ) )
169 fzfi 
 |-  ( 1 ... N ) e. Fin
170 dfii2 
 |-  II = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )
171 iicmp 
 |-  II e. Comp
172 170 171 eqeltrri 
 |-  ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) e. Comp
173 172 fconst6 
 |-  ( ( 1 ... N ) X. { ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) } ) : ( 1 ... N ) --> Comp
174 ptcmpfi 
 |-  ( ( ( 1 ... N ) e. Fin /\ ( ( 1 ... N ) X. { ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) } ) : ( 1 ... N ) --> Comp ) -> ( Xt_ ` ( ( 1 ... N ) X. { ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) } ) ) e. Comp )
175 169 173 174 mp2an 
 |-  ( Xt_ ` ( ( 1 ... N ) X. { ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) } ) ) e. Comp
176 168 175 eqeltri 
 |-  ( R |`t I ) e. Comp
177 rehaus 
 |-  ( topGen ` ran (,) ) e. Haus
178 177 fconst6 
 |-  ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) : ( 1 ... N ) --> Haus
179 pthaus 
 |-  ( ( ( 1 ... N ) e. Fin /\ ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) : ( 1 ... N ) --> Haus ) -> ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ) e. Haus )
180 169 178 179 mp2an 
 |-  ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ) e. Haus
181 3 180 eqeltri 
 |-  R e. Haus
182 haustop 
 |-  ( R e. Haus -> R e. Top )
183 181 182 ax-mp 
 |-  R e. Top
184 reex 
 |-  RR e. _V
185 mapss 
 |-  ( ( RR e. _V /\ ( 0 [,] 1 ) C_ RR ) -> ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) C_ ( RR ^m ( 1 ... N ) ) )
186 184 130 185 mp2an 
 |-  ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) C_ ( RR ^m ( 1 ... N ) )
187 2 186 eqsstri 
 |-  I C_ ( RR ^m ( 1 ... N ) )
188 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
189 3 188 ptuniconst 
 |-  ( ( ( 1 ... N ) e. Fin /\ ( topGen ` ran (,) ) e. Top ) -> ( RR ^m ( 1 ... N ) ) = U. R )
190 169 155 189 mp2an 
 |-  ( RR ^m ( 1 ... N ) ) = U. R
191 190 restuni 
 |-  ( ( R e. Top /\ I C_ ( RR ^m ( 1 ... N ) ) ) -> I = U. ( R |`t I ) )
192 183 187 191 mp2an 
 |-  I = U. ( R |`t I )
193 192 bwth 
 |-  ( ( ( R |`t I ) e. Comp /\ ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) C_ I /\ -. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) e. Fin ) -> E. c e. I c e. ( ( limPt ` ( R |`t I ) ) ` ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) )
194 193 3expia 
 |-  ( ( ( R |`t I ) e. Comp /\ ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) C_ I ) -> ( -. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) e. Fin -> E. c e. I c e. ( ( limPt ` ( R |`t I ) ) ` ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) ) )
195 176 59 194 sylancr 
 |-  ( ph -> ( -. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) e. Fin -> E. c e. I c e. ( ( limPt ` ( R |`t I ) ) ` ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) ) )
196 cmptop 
 |-  ( ( R |`t I ) e. Comp -> ( R |`t I ) e. Top )
197 176 196 ax-mp 
 |-  ( R |`t I ) e. Top
198 192 islp3 
 |-  ( ( ( R |`t I ) e. Top /\ ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) C_ I /\ c e. I ) -> ( c e. ( ( limPt ` ( R |`t I ) ) ` ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) <-> A. v e. ( R |`t I ) ( c e. v -> ( v i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) =/= (/) ) ) )
199 197 198 mp3an1 
 |-  ( ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) C_ I /\ c e. I ) -> ( c e. ( ( limPt ` ( R |`t I ) ) ` ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) <-> A. v e. ( R |`t I ) ( c e. v -> ( v i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) =/= (/) ) ) )
200 59 199 sylan 
 |-  ( ( ph /\ c e. I ) -> ( c e. ( ( limPt ` ( R |`t I ) ) ` ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) <-> A. v e. ( R |`t I ) ( c e. v -> ( v i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) =/= (/) ) ) )
201 fzfid 
 |-  ( ( c e. I /\ i e. NN ) -> ( 1 ... N ) e. Fin )
202 156 a1i 
 |-  ( ( c e. I /\ i e. NN ) -> ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) : ( 1 ... N ) --> Top )
203 nnrecre 
 |-  ( i e. NN -> ( 1 / i ) e. RR )
204 203 rexrd 
 |-  ( i e. NN -> ( 1 / i ) e. RR* )
205 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
206 137 205 tgioo 
 |-  ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
207 206 blopn 
 |-  ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) /\ ( c ` m ) e. RR /\ ( 1 / i ) e. RR* ) -> ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) e. ( topGen ` ran (,) ) )
208 138 207 mp3an1 
 |-  ( ( ( c ` m ) e. RR /\ ( 1 / i ) e. RR* ) -> ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) e. ( topGen ` ran (,) ) )
209 134 204 208 syl2an 
 |-  ( ( ( c e. I /\ m e. ( 1 ... N ) ) /\ i e. NN ) -> ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) e. ( topGen ` ran (,) ) )
210 209 an32s 
 |-  ( ( ( c e. I /\ i e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) e. ( topGen ` ran (,) ) )
211 161 fvconst2 
 |-  ( m e. ( 1 ... N ) -> ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` m ) = ( topGen ` ran (,) ) )
212 211 adantl 
 |-  ( ( ( c e. I /\ i e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` m ) = ( topGen ` ran (,) ) )
213 210 212 eleqtrrd 
 |-  ( ( ( c e. I /\ i e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) e. ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` m ) )
214 noel 
 |-  -. m e. (/)
215 difid 
 |-  ( ( 1 ... N ) \ ( 1 ... N ) ) = (/)
216 215 eleq2i 
 |-  ( m e. ( ( 1 ... N ) \ ( 1 ... N ) ) <-> m e. (/) )
217 214 216 mtbir 
 |-  -. m e. ( ( 1 ... N ) \ ( 1 ... N ) )
218 217 pm2.21i 
 |-  ( m e. ( ( 1 ... N ) \ ( 1 ... N ) ) -> ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) = U. ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` m ) )
219 218 adantl 
 |-  ( ( ( c e. I /\ i e. NN ) /\ m e. ( ( 1 ... N ) \ ( 1 ... N ) ) ) -> ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) = U. ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` m ) )
220 201 202 201 213 219 ptopn 
 |-  ( ( c e. I /\ i e. NN ) -> X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) e. ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ) )
221 220 3 eleqtrrdi 
 |-  ( ( c e. I /\ i e. NN ) -> X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) e. R )
222 ovex 
 |-  ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) e. _V
223 2 222 eqeltri 
 |-  I e. _V
224 elrestr 
 |-  ( ( R e. Haus /\ I e. _V /\ X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) e. R ) -> ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) e. ( R |`t I ) )
225 181 223 224 mp3an12 
 |-  ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) e. R -> ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) e. ( R |`t I ) )
226 221 225 syl 
 |-  ( ( c e. I /\ i e. NN ) -> ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) e. ( R |`t I ) )
227 difss 
 |-  ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) C_ ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) )
228 imassrn 
 |-  ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) C_ ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) )
229 227 228 sstri 
 |-  ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) C_ ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) )
230 229 59 sstrid 
 |-  ( ph -> ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) C_ I )
231 haust1 
 |-  ( R e. Haus -> R e. Fre )
232 181 231 ax-mp 
 |-  R e. Fre
233 restt1 
 |-  ( ( R e. Fre /\ I e. _V ) -> ( R |`t I ) e. Fre )
234 232 223 233 mp2an 
 |-  ( R |`t I ) e. Fre
235 funmpt 
 |-  Fun ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) )
236 imafi 
 |-  ( ( Fun ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ ( 1 ..^ i ) e. Fin ) -> ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) e. Fin )
237 235 116 236 mp2an 
 |-  ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) e. Fin
238 diffi 
 |-  ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) e. Fin -> ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) e. Fin )
239 237 238 ax-mp 
 |-  ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) e. Fin
240 192 t1ficld 
 |-  ( ( ( R |`t I ) e. Fre /\ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) C_ I /\ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) e. Fin ) -> ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) e. ( Clsd ` ( R |`t I ) ) )
241 234 239 240 mp3an13 
 |-  ( ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) C_ I -> ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) e. ( Clsd ` ( R |`t I ) ) )
242 230 241 syl 
 |-  ( ph -> ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) e. ( Clsd ` ( R |`t I ) ) )
243 192 difopn 
 |-  ( ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) e. ( R |`t I ) /\ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) e. ( Clsd ` ( R |`t I ) ) ) -> ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) e. ( R |`t I ) )
244 226 242 243 syl2anr 
 |-  ( ( ph /\ ( c e. I /\ i e. NN ) ) -> ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) e. ( R |`t I ) )
245 244 anassrs 
 |-  ( ( ( ph /\ c e. I ) /\ i e. NN ) -> ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) e. ( R |`t I ) )
246 eleq2 
 |-  ( v = ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) -> ( c e. v <-> c e. ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) ) )
247 ineq1 
 |-  ( v = ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) -> ( v i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) = ( ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) )
248 247 neeq1d 
 |-  ( v = ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) -> ( ( v i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) =/= (/) <-> ( ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) =/= (/) ) )
249 246 248 imbi12d 
 |-  ( v = ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) -> ( ( c e. v -> ( v i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) =/= (/) ) <-> ( c e. ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) -> ( ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) =/= (/) ) ) )
250 249 rspcva 
 |-  ( ( ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) e. ( R |`t I ) /\ A. v e. ( R |`t I ) ( c e. v -> ( v i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) =/= (/) ) ) -> ( c e. ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) -> ( ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) =/= (/) ) )
251 132 ffnd 
 |-  ( c e. I -> c Fn ( 1 ... N ) )
252 251 adantr 
 |-  ( ( c e. I /\ i e. NN ) -> c Fn ( 1 ... N ) )
253 142 ralrimiva 
 |-  ( ( c e. I /\ i e. NN ) -> A. m e. ( 1 ... N ) ( c ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) )
254 108 elixp 
 |-  ( c e. X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) <-> ( c Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( c ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
255 252 253 254 sylanbrc 
 |-  ( ( c e. I /\ i e. NN ) -> c e. X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) )
256 simpl 
 |-  ( ( c e. I /\ i e. NN ) -> c e. I )
257 255 256 elind 
 |-  ( ( c e. I /\ i e. NN ) -> c e. ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) )
258 neldifsnd 
 |-  ( ( c e. I /\ i e. NN ) -> -. c e. ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) )
259 257 258 eldifd 
 |-  ( ( c e. I /\ i e. NN ) -> c e. ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) )
260 259 adantll 
 |-  ( ( ( ph /\ c e. I ) /\ i e. NN ) -> c e. ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) )
261 simplr 
 |-  ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) -> A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) )
262 261 anim1i 
 |-  ( ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) -> ( A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) /\ -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) )
263 simpl 
 |-  ( ( j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ -. j e. { c } ) -> j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) )
264 262 263 anim12i 
 |-  ( ( ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) /\ ( j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ -. j e. { c } ) ) -> ( ( A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) /\ -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) /\ j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) )
265 elin 
 |-  ( j e. ( ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) <-> ( j e. ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) /\ j e. ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) )
266 andir 
 |-  ( ( ( ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) \/ ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. -. j e. { c } ) ) /\ ( j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ -. j e. { c } ) ) <-> ( ( ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) /\ ( j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ -. j e. { c } ) ) \/ ( ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. -. j e. { c } ) /\ ( j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ -. j e. { c } ) ) ) )
267 eldif 
 |-  ( j e. ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) <-> ( j e. ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) /\ -. j e. ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) )
268 elin 
 |-  ( j e. ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) <-> ( j e. X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) /\ j e. I ) )
269 vex 
 |-  j e. _V
270 269 elixp 
 |-  ( j e. X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) <-> ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
271 270 anbi1i 
 |-  ( ( j e. X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) /\ j e. I ) <-> ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) )
272 268 271 bitri 
 |-  ( j e. ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) <-> ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) )
273 ianor 
 |-  ( -. ( j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) /\ -. j e. { c } ) <-> ( -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \/ -. -. j e. { c } ) )
274 eldif 
 |-  ( j e. ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) <-> ( j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) /\ -. j e. { c } ) )
275 273 274 xchnxbir 
 |-  ( -. j e. ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) <-> ( -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \/ -. -. j e. { c } ) )
276 272 275 anbi12i 
 |-  ( ( j e. ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) /\ -. j e. ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) <-> ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ ( -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \/ -. -. j e. { c } ) ) )
277 andi 
 |-  ( ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ ( -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \/ -. -. j e. { c } ) ) <-> ( ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) \/ ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. -. j e. { c } ) ) )
278 267 276 277 3bitri 
 |-  ( j e. ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) <-> ( ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) \/ ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. -. j e. { c } ) ) )
279 eldif 
 |-  ( j e. ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) <-> ( j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ -. j e. { c } ) )
280 278 279 anbi12i 
 |-  ( ( j e. ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) /\ j e. ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) <-> ( ( ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) \/ ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. -. j e. { c } ) ) /\ ( j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ -. j e. { c } ) ) )
281 pm3.24 
 |-  -. ( -. j e. { c } /\ -. -. j e. { c } )
282 simpr 
 |-  ( ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. -. j e. { c } ) -> -. -. j e. { c } )
283 simpr 
 |-  ( ( j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ -. j e. { c } ) -> -. j e. { c } )
284 282 283 anim12ci 
 |-  ( ( ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. -. j e. { c } ) /\ ( j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ -. j e. { c } ) ) -> ( -. j e. { c } /\ -. -. j e. { c } ) )
285 281 284 mto 
 |-  -. ( ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. -. j e. { c } ) /\ ( j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ -. j e. { c } ) )
286 285 biorfri 
 |-  ( ( ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) /\ ( j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ -. j e. { c } ) ) <-> ( ( ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) /\ ( j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ -. j e. { c } ) ) \/ ( ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. -. j e. { c } ) /\ ( j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ -. j e. { c } ) ) ) )
287 266 280 286 3bitr4i 
 |-  ( ( j e. ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) /\ j e. ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) <-> ( ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) /\ ( j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ -. j e. { c } ) ) )
288 265 287 bitri 
 |-  ( j e. ( ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) <-> ( ( ( ( j Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) /\ j e. I ) /\ -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) /\ ( j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ -. j e. { c } ) ) )
289 ancom 
 |-  ( ( ( -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) /\ j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) <-> ( A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) /\ ( -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) /\ j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) ) )
290 anass 
 |-  ( ( ( A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) /\ -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) /\ j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) <-> ( A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) /\ ( -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) /\ j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) ) )
291 289 290 bitr4i 
 |-  ( ( ( -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) /\ j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) <-> ( ( A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) /\ -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) /\ j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) )
292 264 288 291 3imtr4i 
 |-  ( j e. ( ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) -> ( ( -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) /\ j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
293 ancom 
 |-  ( ( -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) /\ j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) <-> ( j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) )
294 eldif 
 |-  ( j e. ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) <-> ( j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) )
295 293 294 bitr4i 
 |-  ( ( -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) /\ j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) <-> j e. ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) )
296 imadmrn 
 |-  ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " dom ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) = ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) )
297 67 68 dmmpti 
 |-  dom ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) = NN
298 297 imaeq2i 
 |-  ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " dom ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) = ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " NN )
299 296 298 eqtr3i 
 |-  ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) = ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " NN )
300 299 difeq1i 
 |-  ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) = ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " NN ) \ ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) )
301 imadifss 
 |-  ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " NN ) \ ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) C_ ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( NN \ ( 1 ..^ i ) ) )
302 300 301 eqsstri 
 |-  ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) C_ ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( NN \ ( 1 ..^ i ) ) )
303 imass2 
 |-  ( ( NN \ ( 1 ..^ i ) ) C_ ( ZZ>= ` i ) -> ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( NN \ ( 1 ..^ i ) ) ) C_ ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( ZZ>= ` i ) ) )
304 97 303 syl 
 |-  ( i e. NN -> ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( NN \ ( 1 ..^ i ) ) ) C_ ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( ZZ>= ` i ) ) )
305 df-ima 
 |-  ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( ZZ>= ` i ) ) = ran ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) |` ( ZZ>= ` i ) )
306 uznnssnn 
 |-  ( i e. NN -> ( ZZ>= ` i ) C_ NN )
307 306 resmptd 
 |-  ( i e. NN -> ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) |` ( ZZ>= ` i ) ) = ( k e. ( ZZ>= ` i ) |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) )
308 307 rneqd 
 |-  ( i e. NN -> ran ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) |` ( ZZ>= ` i ) ) = ran ( k e. ( ZZ>= ` i ) |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) )
309 305 308 eqtrid 
 |-  ( i e. NN -> ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( ZZ>= ` i ) ) = ran ( k e. ( ZZ>= ` i ) |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) )
310 304 309 sseqtrd 
 |-  ( i e. NN -> ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( NN \ ( 1 ..^ i ) ) ) C_ ran ( k e. ( ZZ>= ` i ) |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) )
311 302 310 sstrid 
 |-  ( i e. NN -> ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) C_ ran ( k e. ( ZZ>= ` i ) |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) )
312 311 sseld 
 |-  ( i e. NN -> ( j e. ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) ) -> j e. ran ( k e. ( ZZ>= ` i ) |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) )
313 295 312 biimtrid 
 |-  ( i e. NN -> ( ( -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) /\ j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) -> j e. ran ( k e. ( ZZ>= ` i ) |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) )
314 313 anim1d 
 |-  ( i e. NN -> ( ( ( -. j e. ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) /\ j e. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) -> ( j e. ran ( k e. ( ZZ>= ` i ) |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) ) )
315 292 314 syl5 
 |-  ( i e. NN -> ( j e. ( ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) -> ( j e. ran ( k e. ( ZZ>= ` i ) |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) ) )
316 315 eximdv 
 |-  ( i e. NN -> ( E. j j e. ( ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) -> E. j ( j e. ran ( k e. ( ZZ>= ` i ) |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) ) )
317 n0 
 |-  ( ( ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) =/= (/) <-> E. j j e. ( ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) )
318 67 rgenw 
 |-  A. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) e. _V
319 eqid 
 |-  ( k e. ( ZZ>= ` i ) |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) = ( k e. ( ZZ>= ` i ) |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) )
320 fveq1 
 |-  ( j = ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) -> ( j ` m ) = ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) )
321 320 eleq1d 
 |-  ( j = ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) -> ( ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) <-> ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
322 321 ralbidv 
 |-  ( j = ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) -> ( A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) <-> A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
323 319 322 rexrnmptw 
 |-  ( A. k e. ( ZZ>= ` i ) ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) e. _V -> ( E. j e. ran ( k e. ( ZZ>= ` i ) |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) <-> E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
324 318 323 ax-mp 
 |-  ( E. j e. ran ( k e. ( ZZ>= ` i ) |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) <-> E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) )
325 df-rex 
 |-  ( E. j e. ran ( k e. ( ZZ>= ` i ) |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) <-> E. j ( j e. ran ( k e. ( ZZ>= ` i ) |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
326 324 325 bitr3i 
 |-  ( E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) <-> E. j ( j e. ran ( k e. ( ZZ>= ` i ) |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) /\ A. m e. ( 1 ... N ) ( j ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
327 316 317 326 3imtr4g 
 |-  ( i e. NN -> ( ( ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) =/= (/) -> E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
328 327 adantl 
 |-  ( ( ( ph /\ c e. I ) /\ i e. NN ) -> ( ( ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) =/= (/) -> E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
329 260 328 embantd 
 |-  ( ( ( ph /\ c e. I ) /\ i e. NN ) -> ( ( c e. ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) -> ( ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) =/= (/) ) -> E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
330 250 329 syl5 
 |-  ( ( ( ph /\ c e. I ) /\ i e. NN ) -> ( ( ( ( X_ m e. ( 1 ... N ) ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) i^i I ) \ ( ( ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) " ( 1 ..^ i ) ) \ { c } ) ) e. ( R |`t I ) /\ A. v e. ( R |`t I ) ( c e. v -> ( v i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) =/= (/) ) ) -> E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
331 245 330 mpand 
 |-  ( ( ( ph /\ c e. I ) /\ i e. NN ) -> ( A. v e. ( R |`t I ) ( c e. v -> ( v i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) =/= (/) ) -> E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
332 331 ralrimdva 
 |-  ( ( ph /\ c e. I ) -> ( A. v e. ( R |`t I ) ( c e. v -> ( v i^i ( ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) \ { c } ) ) =/= (/) ) -> A. i e. NN E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
333 200 332 sylbid 
 |-  ( ( ph /\ c e. I ) -> ( c e. ( ( limPt ` ( R |`t I ) ) ` ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) -> A. i e. NN E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
334 333 reximdva 
 |-  ( ph -> ( E. c e. I c e. ( ( limPt ` ( R |`t I ) ) ` ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ) -> E. c e. I A. i e. NN E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
335 195 334 syld 
 |-  ( ph -> ( -. ran ( k e. NN |-> ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) e. Fin -> E. c e. I A. i e. NN E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) ) )
336 150 335 pm2.61d 
 |-  ( ph -> E. c e. I A. i e. NN E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) )
337 1 2 3 4 5 6 7 8 poimirlem29 
 |-  ( ph -> ( A. i e. NN E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) -> A. n e. ( 1 ... N ) A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) )
338 337 reximdv 
 |-  ( ph -> ( E. c e. I A. i e. NN E. k e. ( ZZ>= ` i ) A. m e. ( 1 ... N ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( c ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / i ) ) -> E. c e. I A. n e. ( 1 ... N ) A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) )
339 336 338 mpd 
 |-  ( ph -> E. c e. I A. n e. ( 1 ... N ) A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )