Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem30 Structured version   Unicode version

Theorem poimirlem30 31884
Description: Lemma for poimir 31887 combining poimirlem29 31883 with bwth 20412. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
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.  ( ( Rt  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
Ref Expression
poimirlem30  |-  ( ph  ->  E. c  e.  I  A. n  e.  (
1 ... N ) A. v  e.  ( Rt  I
) ( c  e.  v  ->  A. r  e.  {  <_  ,  `'  <_  } E. z  e.  v  0 r ( ( F `  z
) `  n )
) )
Distinct variable groups:    f, j,
k, n, z    ph, j, n    j, F, n    j, N, n    ph, k    f, N, k    ph, z    f, F, k, z    z, N   
j, c, k, n, r, v, z, ph    f, c, F, r, v    G, c, f, j, k, n, r, v, z   
I, c, f, j, k, n, r, v, z    N, c, r, v    R, c, f, j, k, n, r, v, z    X, c, f, r, v, z
Allowed substitution hints:    ph( f)    X( j, k, n)

Proof of Theorem poimirlem30
Dummy variables  i  m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfzonn0 11961 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 0..^ k )  ->  i  e.  NN0 )
21nn0red 10927 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0..^ k )  ->  i  e.  RR )
3 nndivre 10646 . . . . . . . . . . . . . . 15  |-  ( ( i  e.  RR  /\  k  e.  NN )  ->  ( i  /  k
)  e.  RR )
42, 3sylan 473 . . . . . . . . . . . . . 14  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  (
i  /  k )  e.  RR )
5 elfzole1 11929 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 0..^ k )  ->  0  <_  i )
62, 5jca 534 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0..^ k )  ->  ( i  e.  RR  /\  0  <_ 
i ) )
7 nnrp 11312 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  k  e.  RR+ )
87rpregt0d 11348 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN  ->  (
k  e.  RR  /\  0  <  k ) )
9 divge0 10475 . . . . . . . . . . . . . . 15  |-  ( ( ( i  e.  RR  /\  0  <_  i )  /\  ( k  e.  RR  /\  0  <  k ) )  ->  0  <_  ( i  /  k ) )
106, 8, 9syl2an 479 . . . . . . . . . . . . . 14  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  0  <_  ( i  /  k
) )
11 elfzo0le 11960 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 0..^ k )  ->  i  <_  k )
1211adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  i  <_  k )
132adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  i  e.  RR )
14 1red 9659 . . . . . . . . . . . . . . . . 17  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  1  e.  RR )
157adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  k  e.  RR+ )
1613, 14, 15ledivmuld 11392 . . . . . . . . . . . . . . . 16  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  (
( i  /  k
)  <_  1  <->  i  <_  ( k  x.  1 ) ) )
17 nncn 10618 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  NN  ->  k  e.  CC )
1817mulid1d 9661 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  NN  ->  (
k  x.  1 )  =  k )
1918breq2d 4432 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  NN  ->  (
i  <_  ( k  x.  1 )  <->  i  <_  k ) )
2019adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  (
i  <_  ( k  x.  1 )  <->  i  <_  k ) )
2116, 20bitrd 256 . . . . . . . . . . . . . . 15  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  (
( i  /  k
)  <_  1  <->  i  <_  k ) )
2212, 21mpbird 235 . . . . . . . . . . . . . 14  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  (
i  /  k )  <_  1 )
23 0re 9644 . . . . . . . . . . . . . . 15  |-  0  e.  RR
24 1re 9643 . . . . . . . . . . . . . . 15  |-  1  e.  RR
2523, 24elicc2i 11701 . . . . . . . . . . . . . 14  |-  ( ( i  /  k )  e.  ( 0 [,] 1 )  <->  ( (
i  /  k )  e.  RR  /\  0  <_  ( i  /  k
)  /\  ( i  /  k )  <_ 
1 ) )
264, 10, 22, 25syl3anbrc 1189 . . . . . . . . . . . . 13  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  (
i  /  k )  e.  ( 0 [,] 1 ) )
2726ancoms 454 . . . . . . . . . . . 12  |-  ( ( k  e.  NN  /\  i  e.  ( 0..^ k ) )  -> 
( i  /  k
)  e.  ( 0 [,] 1 ) )
28 elsni 4021 . . . . . . . . . . . . . 14  |-  ( j  e.  { k }  ->  j  =  k )
2928oveq2d 6318 . . . . . . . . . . . . 13  |-  ( j  e.  { k }  ->  ( i  / 
j )  =  ( i  /  k ) )
3029eleq1d 2491 . . . . . . . . . . . 12  |-  ( j  e.  { k }  ->  ( ( i  /  j )  e.  ( 0 [,] 1
)  <->  ( i  / 
k )  e.  ( 0 [,] 1 ) ) )
3127, 30syl5ibrcom 225 . . . . . . . . . . 11  |-  ( ( k  e.  NN  /\  i  e.  ( 0..^ k ) )  -> 
( j  e.  {
k }  ->  (
i  /  j )  e.  ( 0 [,] 1 ) ) )
3231impr 623 . . . . . . . . . 10  |-  ( ( k  e.  NN  /\  ( i  e.  ( 0..^ k )  /\  j  e.  { k } ) )  -> 
( i  /  j
)  e.  ( 0 [,] 1 ) )
3332adantll 718 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
i  e.  ( 0..^ k )  /\  j  e.  { k } ) )  ->  ( i  /  j )  e.  ( 0 [,] 1
) )
34 poimirlem30.2 . . . . . . . . . . . 12  |-  ( ph  ->  G : NN --> ( ( NN0  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
3534ffvelrnda 6034 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( G `
 k )  e.  ( ( NN0  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } ) )
36 xp1st 6834 . . . . . . . . . . 11  |-  ( ( 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 ) ) )
37 elmapfn 7499 . . . . . . . . . . 11  |-  ( ( 1st `  ( G `
 k ) )  e.  ( NN0  ^m  ( 1 ... N
) )  ->  ( 1st `  ( G `  k ) )  Fn  ( 1 ... N
) )
3835, 36, 373syl 18 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1st `  ( G `  k
) )  Fn  (
1 ... N ) )
39 poimirlem30.3 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  ran  ( 1st `  ( G `  k ) )  C_  ( 0..^ k ) )
40 df-f 5602 . . . . . . . . . 10  |-  ( ( 1st `  ( G `
 k ) ) : ( 1 ... N ) --> ( 0..^ k )  <->  ( ( 1st `  ( G `  k ) )  Fn  ( 1 ... N
)  /\  ran  ( 1st `  ( G `  k
) )  C_  (
0..^ k ) ) )
4138, 39, 40sylanbrc 668 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1st `  ( G `  k
) ) : ( 1 ... N ) --> ( 0..^ k ) )
42 vex 3084 . . . . . . . . . . 11  |-  k  e. 
_V
4342fconst 5783 . . . . . . . . . 10  |-  ( ( 1 ... N )  X.  { k } ) : ( 1 ... N ) --> { k }
4443a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 1 ... N )  X.  { k } ) : ( 1 ... N ) --> { k } )
45 fzfid 12186 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1 ... N )  e. 
Fin )
46 inidm 3671 . . . . . . . . 9  |-  ( ( 1 ... N )  i^i  ( 1 ... N ) )  =  ( 1 ... N
)
4733, 41, 44, 45, 45, 46off 6557 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) : ( 1 ... N
) --> ( 0 [,] 1 ) )
48 poimir.i . . . . . . . . . 10  |-  I  =  ( ( 0 [,] 1 )  ^m  (
1 ... N ) )
4948eleq2i 2500 . . . . . . . . 9  |-  ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  e.  I  <->  ( ( 1st `  ( G `  k ) )  oF  /  ( ( 1 ... N )  X.  { k } ) )  e.  ( ( 0 [,] 1
)  ^m  ( 1 ... N ) ) )
50 ovex 6330 . . . . . . . . . 10  |-  ( 0 [,] 1 )  e. 
_V
51 ovex 6330 . . . . . . . . . 10  |-  ( 1 ... N )  e. 
_V
5250, 51elmap 7505 . . . . . . . . 9  |-  ( ( ( 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
) )
5349, 52bitri 252 . . . . . . . 8  |-  ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  e.  I  <->  ( ( 1st `  ( G `  k ) )  oF  /  ( ( 1 ... N )  X.  { k } ) ) : ( 1 ... N ) --> ( 0 [,] 1
) )
5447, 53sylibr 215 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) )  e.  I )
55 eqid 2422 . . . . . . 7  |-  ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )  =  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) )
5654, 55fmptd 6058 . . . . . 6  |-  ( ph  ->  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) : NN --> I )
57 frn 5749 . . . . . 6  |-  ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) : NN --> I  ->  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  C_  I )
5856, 57syl 17 . . . . 5  |-  ( ph  ->  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) )  C_  I
)
59 ominf 7787 . . . . . . 7  |-  -.  om  e.  Fin
60 nnenom 12193 . . . . . . . . 9  |-  NN  ~~  om
61 enfi 7791 . . . . . . . . 9  |-  ( NN 
~~  om  ->  ( NN  e.  Fin  <->  om  e.  Fin ) )
6260, 61ax-mp 5 . . . . . . . 8  |-  ( NN  e.  Fin  <->  om  e.  Fin )
63 iunid 4351 . . . . . . . . . . 11  |-  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 } ) ) )
6463imaeq2i 5182 . . . . . . . . . 10  |-  ( `' ( 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 } ) ) ) )
65 imaiun 6162 . . . . . . . . . 10  |-  ( `' ( 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 } )
66 ovex 6330 . . . . . . . . . . . . 13  |-  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) )  e. 
_V
6766, 55fnmpti 5721 . . . . . . . . . . . 12  |-  ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )  Fn  NN
68 dffn3 5750 . . . . . . . . . . . 12  |-  ( ( 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 } ) ) ) )
6967, 68mpbi 211 . . . . . . . . . . 11  |-  ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) : NN --> ran  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )
70 fimacnv 6024 . . . . . . . . . . 11  |-  ( ( 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 )
7169, 70ax-mp 5 . . . . . . . . . 10  |-  ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ran  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) )  =  NN
7264, 65, 713eqtr3ri 2460 . . . . . . . . 9  |-  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 } )
7372eleq1i 2499 . . . . . . . 8  |-  ( 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 )
7462, 73bitr3i 254 . . . . . . 7  |-  ( 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 )
7559, 74mtbi 299 . . . . . 6  |-  -.  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 ralnex 2871 . . . . . . . . . . . 12  |-  ( 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 )
7776rexbii 2927 . . . . . . . . . . 11  |-  ( 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 )
78 rexnal 2873 . . . . . . . . . . 11  |-  ( 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 )
7977, 78bitri 252 . . . . . . . . . 10  |-  ( 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 )
8079ralbii 2856 . . . . . . . . 9  |-  ( 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 )
81 ralnex 2871 . . . . . . . . 9  |-  ( 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 )
8280, 81bitri 252 . . . . . . . 8  |-  ( 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 )
83 nnuz 11195 . . . . . . . . . . . . . . . 16  |-  NN  =  ( ZZ>= `  1 )
84 elnnuz 11196 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  NN  <->  i  e.  ( ZZ>= `  1 )
)
85 fzouzsplit 11954 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( ZZ>= `  1
)  ->  ( ZZ>= ` 
1 )  =  ( ( 1..^ i )  u.  ( ZZ>= `  i
) ) )
8684, 85sylbi 198 . . . . . . . . . . . . . . . 16  |-  ( i  e.  NN  ->  ( ZZ>=
`  1 )  =  ( ( 1..^ i )  u.  ( ZZ>= `  i ) ) )
8783, 86syl5eq 2475 . . . . . . . . . . . . . . 15  |-  ( i  e.  NN  ->  NN  =  ( ( 1..^ i )  u.  ( ZZ>=
`  i ) ) )
8887difeq1d 3582 . . . . . . . . . . . . . 14  |-  ( i  e.  NN  ->  ( NN  \  ( 1..^ i ) )  =  ( ( ( 1..^ i )  u.  ( ZZ>= `  i ) )  \ 
( 1..^ i ) ) )
89 uncom 3610 . . . . . . . . . . . . . . . 16  |-  ( ( 1..^ i )  u.  ( ZZ>= `  i )
)  =  ( (
ZZ>= `  i )  u.  ( 1..^ i ) )
9089difeq1i 3579 . . . . . . . . . . . . . . 15  |-  ( ( ( 1..^ i )  u.  ( ZZ>= `  i
) )  \  (
1..^ i ) )  =  ( ( (
ZZ>= `  i )  u.  ( 1..^ i ) )  \  ( 1..^ i ) )
91 difun2 3875 . . . . . . . . . . . . . . 15  |-  ( ( ( ZZ>= `  i )  u.  ( 1..^ i ) )  \  ( 1..^ i ) )  =  ( ( ZZ>= `  i
)  \  ( 1..^ i ) )
9290, 91eqtri 2451 . . . . . . . . . . . . . 14  |-  ( ( ( 1..^ i )  u.  ( ZZ>= `  i
) )  \  (
1..^ i ) )  =  ( ( ZZ>= `  i )  \  (
1..^ i ) )
9388, 92syl6eq 2479 . . . . . . . . . . . . 13  |-  ( i  e.  NN  ->  ( NN  \  ( 1..^ i ) )  =  ( ( ZZ>= `  i )  \  ( 1..^ i ) ) )
94 difss 3592 . . . . . . . . . . . . 13  |-  ( (
ZZ>= `  i )  \ 
( 1..^ i ) )  C_  ( ZZ>= `  i )
9593, 94syl6eqss 3514 . . . . . . . . . . . 12  |-  ( i  e.  NN  ->  ( NN  \  ( 1..^ i ) )  C_  ( ZZ>=
`  i ) )
96 ssralv 3525 . . . . . . . . . . . 12  |-  ( ( 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 ) )
9795, 96syl 17 . . . . . . . . . . 11  |-  ( 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 ) )
98 impexp 447 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) )
99 eldif 3446 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( NN  \ 
( 1..^ i ) )  <->  ( k  e.  NN  /\  -.  k  e.  ( 1..^ i ) ) )
10099imbi1i 326 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) )
101 con34b 293 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) )
102101imbi2i 313 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) ) )
10398, 100, 1023bitr4i 280 . . . . . . . . . . . . . 14  |-  ( ( 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 ) ) ) )
104103albii 1687 . . . . . . . . . . . . 13  |-  ( 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 ) ) ) )
105 df-ral 2780 . . . . . . . . . . . . 13  |-  ( 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 ) )
106 vex 3084 . . . . . . . . . . . . . . . 16  |-  c  e. 
_V
10755mptiniseg 5345 . . . . . . . . . . . . . . . 16  |-  ( 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 } )
108106, 107ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " { c } )  =  {
k  e.  NN  | 
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c }
109108sseq1i 3488 . . . . . . . . . . . . . 14  |-  ( ( `' ( 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 ) )
110 rabss 3538 . . . . . . . . . . . . . 14  |-  ( { 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 ) ) )
111 df-ral 2780 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) )
112109, 110, 1113bitri 274 . . . . . . . . . . . . 13  |-  ( ( `' ( 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 ) ) ) )
113104, 105, 1123bitr4i 280 . . . . . . . . . . . 12  |-  ( 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 ) )
114 fzofi 12187 . . . . . . . . . . . . 13  |-  ( 1..^ i )  e.  Fin
115 ssfi 7795 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
116114, 115mpan 674 . . . . . . . . . . . 12  |-  ( ( `' ( 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 )
117113, 116sylbi 198 . . . . . . . . . . 11  |-  ( 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 )
11897, 117syl6 34 . . . . . . . . . 10  |-  ( 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 ) )
119118rexlimiv 2911 . . . . . . . . 9  |-  ( 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 )
120119ralimi 2818 . . . . . . . 8  |-  ( 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 )
12182, 120sylbir 216 . . . . . . 7  |-  ( -. 
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 )
122 iunfi 7865 . . . . . . . 8  |-  ( ( 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 )
123122ex 435 . . . . . . 7  |-  ( 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 ) )
124121, 123syl5 33 . . . . . 6  |-  ( 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 ) )
12575, 124mt3i 129 . . . . 5  |-  ( 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 )
126 ssrexv 3526 . . . . 5  |-  ( 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 ) )
12758, 125, 126syl2im 39 . . . 4  |-  ( 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 ) )
128 unitssre 11780 . . . . . . . . . . . 12  |-  ( 0 [,] 1 )  C_  RR
129 elmapi 7498 . . . . . . . . . . . . . 14  |-  ( c  e.  ( ( 0 [,] 1 )  ^m  ( 1 ... N
) )  ->  c : ( 1 ... N ) --> ( 0 [,] 1 ) )
130129, 48eleq2s 2530 . . . . . . . . . . . . 13  |-  ( c  e.  I  ->  c : ( 1 ... N ) --> ( 0 [,] 1 ) )
131130ffvelrnda 6034 . . . . . . . . . . . 12  |-  ( ( c  e.  I  /\  m  e.  ( 1 ... N ) )  ->  ( c `  m )  e.  ( 0 [,] 1 ) )
132128, 131sseldi 3462 . . . . . . . . . . 11  |-  ( ( c  e.  I  /\  m  e.  ( 1 ... N ) )  ->  ( c `  m )  e.  RR )
133 nnrp 11312 . . . . . . . . . . . 12  |-  ( i  e.  NN  ->  i  e.  RR+ )
134133rpreccld 11352 . . . . . . . . . . 11  |-  ( i  e.  NN  ->  (
1  /  i )  e.  RR+ )
135 eqid 2422 . . . . . . . . . . . . 13  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  =  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )
136135rexmet 21796 . . . . . . . . . . . 12  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  e.  ( *Met `  RR )
137 blcntr 21415 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) ) )
138136, 137mp3an1 1347 . . . . . . . . . . 11  |-  ( ( ( c `  m
)  e.  RR  /\  ( 1  /  i
)  e.  RR+ )  ->  ( c `  m
)  e.  ( ( c `  m ) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) ) )
139132, 134, 138syl2an 479 . . . . . . . . . 10  |-  ( ( ( c  e.  I  /\  m  e.  (
1 ... N ) )  /\  i  e.  NN )  ->  ( c `  m )  e.  ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) ) )
140139an32s 811 . . . . . . . . 9  |-  ( ( ( c  e.  I  /\  i  e.  NN )  /\  m  e.  ( 1 ... N ) )  ->  ( c `  m )  e.  ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) ) )
141 fveq1 5877 . . . . . . . . . 10  |-  ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  (
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) `
 m )  =  ( c `  m
) )
142141eleq1d 2491 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) )
143140, 142syl5ibrcom 225 . . . . . . . 8  |-  ( ( ( 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 ) ) ) )
144143ralrimdva 2843 . . . . . . 7  |-  ( ( 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 ) ) ) )
145144reximdv 2899 . . . . . 6  |-  ( ( 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 ) ) ) )
146145ralimdva 2833 . . . . 5  |-  ( 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 ) ) ) )
147146reximia 2891 . . . 4  |-  ( 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 ) ) )
148127, 147syl6 34 . . 3  |-  ( 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 ) ) ) )
149 poimir.r . . . . . . . 8  |-  R  =  ( Xt_ `  (
( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) )
15051, 50ixpconst 7537 . . . . . . . . 9  |-  X_ n  e.  ( 1 ... N
) ( 0 [,] 1 )  =  ( ( 0 [,] 1
)  ^m  ( 1 ... N ) )
15148, 150eqtr4i 2454 . . . . . . . 8  |-  I  = 
X_ n  e.  ( 1 ... N ) ( 0 [,] 1
)
152149, 151oveq12i 6314 . . . . . . 7  |-  ( Rt  I )  =  ( (
Xt_ `  ( (
1 ... N )  X. 
{ ( topGen `  ran  (,) ) } ) )t  X_ n  e.  ( 1 ... N ) ( 0 [,] 1 ) )
153 fzfid 12186 . . . . . . . . 9  |-  ( T. 
->  ( 1 ... N
)  e.  Fin )
154 retop 21769 . . . . . . . . . . 11  |-  ( topGen ` 
ran  (,) )  e.  Top
155154fconst6 5787 . . . . . . . . . 10  |-  ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) : ( 1 ... N ) --> Top
156155a1i 11 . . . . . . . . 9  |-  ( T. 
->  ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) : ( 1 ... N ) --> Top )
15750a1i 11 . . . . . . . . 9  |-  ( ( T.  /\  n  e.  ( 1 ... N
) )  ->  (
0 [,] 1 )  e.  _V )
158153, 156, 157ptrest 31853 . . . . . . . 8  |-  ( 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 ) ) ) ) )
159158trud 1446 . . . . . . 7  |-  ( (
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 fvex 5888 . . . . . . . . . . . 12  |-  ( topGen ` 
ran  (,) )  e.  _V
161160fvconst2 6132 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... N )  ->  (
( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  n
)  =  ( topGen ` 
ran  (,) ) )
162161oveq1d 6317 . . . . . . . . . 10  |-  ( n  e.  ( 1 ... N )  ->  (
( ( ( 1 ... N )  X. 
{ ( topGen `  ran  (,) ) } ) `  n )t  ( 0 [,] 1 ) )  =  ( ( topGen `  ran  (,) )t  ( 0 [,] 1
) ) )
163162mpteq2ia 4503 . . . . . . . . 9  |-  ( n  e.  ( 1 ... N )  |->  ( ( ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  n
)t  ( 0 [,] 1
) ) )  =  ( n  e.  ( 1 ... N ) 
|->  ( ( topGen `  ran  (,) )t  ( 0 [,] 1
) ) )
164 fconstmpt 4894 . . . . . . . . 9  |-  ( ( 1 ... N )  X.  { ( (
topGen `  ran  (,) )t  (
0 [,] 1 ) ) } )  =  ( n  e.  ( 1 ... N ) 
|->  ( ( topGen `  ran  (,) )t  ( 0 [,] 1
) ) )
165163, 164eqtr4i 2454 . . . . . . . 8  |-  ( n  e.  ( 1 ... N )  |->  ( ( ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  n
)t  ( 0 [,] 1
) ) )  =  ( ( 1 ... N )  X.  {
( ( topGen `  ran  (,) )t  ( 0 [,] 1
) ) } )
166165fveq2i 5881 . . . . . . 7  |-  ( Xt_ `  ( n  e.  ( 1 ... N ) 
|->  ( ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )t  ( 0 [,] 1 ) ) ) )  =  (
Xt_ `  ( (
1 ... N )  X. 
{ ( ( topGen ` 
ran  (,) )t  ( 0 [,] 1 ) ) } ) )
167152, 159, 1663eqtri 2455 . . . . . 6  |-  ( Rt  I )  =  ( Xt_ `  ( ( 1 ... N )  X.  {
( ( topGen `  ran  (,) )t  ( 0 [,] 1
) ) } ) )
168 fzfi 12185 . . . . . . 7  |-  ( 1 ... N )  e. 
Fin
169 dfii2 21901 . . . . . . . . 9  |-  II  =  ( ( topGen `  ran  (,) )t  ( 0 [,] 1
) )
170 iicmp 21905 . . . . . . . . 9  |-  II  e.  Comp
171169, 170eqeltrri 2507 . . . . . . . 8  |-  ( (
topGen `  ran  (,) )t  (
0 [,] 1 ) )  e.  Comp
172171fconst6 5787 . . . . . . 7  |-  ( ( 1 ... N )  X.  { ( (
topGen `  ran  (,) )t  (
0 [,] 1 ) ) } ) : ( 1 ... N
) --> Comp
173 ptcmpfi 20815 . . . . . . 7  |-  ( ( ( 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 )
174168, 172, 173mp2an 676 . . . . . 6  |-  ( Xt_ `  ( ( 1 ... N )  X.  {
( ( topGen `  ran  (,) )t  ( 0 [,] 1
) ) } ) )  e.  Comp
175167, 174eqeltri 2506 . . . . 5  |-  ( Rt  I )  e.  Comp
176 rehaus 21804 . . . . . . . . . . . 12  |-  ( topGen ` 
ran  (,) )  e.  Haus
177176fconst6 5787 . . . . . . . . . . 11  |-  ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) : ( 1 ... N ) --> Haus
178 pthaus 20640 . . . . . . . . . . 11  |-  ( ( ( 1 ... N
)  e.  Fin  /\  ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) : ( 1 ... N ) -->
Haus )  ->  ( Xt_ `  ( ( 1 ... N )  X. 
{ ( topGen `  ran  (,) ) } ) )  e.  Haus )
179168, 177, 178mp2an 676 . . . . . . . . . 10  |-  ( Xt_ `  ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) )  e. 
Haus
180149, 179eqeltri 2506 . . . . . . . . 9  |-  R  e. 
Haus
181 haustop 20334 . . . . . . . . 9  |-  ( R  e.  Haus  ->  R  e. 
Top )
182180, 181ax-mp 5 . . . . . . . 8  |-  R  e. 
Top
183 reex 9631 . . . . . . . . . 10  |-  RR  e.  _V
184 mapss 7519 . . . . . . . . . 10  |-  ( ( RR  e.  _V  /\  ( 0 [,] 1
)  C_  RR )  ->  ( ( 0 [,] 1 )  ^m  (
1 ... N ) ) 
C_  ( RR  ^m  ( 1 ... N
) ) )
185183, 128, 184mp2an 676 . . . . . . . . 9  |-  ( ( 0 [,] 1 )  ^m  ( 1 ... N ) )  C_  ( RR  ^m  (
1 ... N ) )
18648, 185eqsstri 3494 . . . . . . . 8  |-  I  C_  ( RR  ^m  (
1 ... N ) )
187 uniretop 21770 . . . . . . . . . . 11  |-  RR  =  U. ( topGen `  ran  (,) )
188149, 187ptuniconst 20600 . . . . . . . . . 10  |-  ( ( ( 1 ... N
)  e.  Fin  /\  ( topGen `  ran  (,) )  e.  Top )  ->  ( RR  ^m  ( 1 ... N ) )  = 
U. R )
189168, 154, 188mp2an 676 . . . . . . . . 9  |-  ( RR 
^m  ( 1 ... N ) )  = 
U. R
190189restuni 20165 . . . . . . . 8  |-  ( ( R  e.  Top  /\  I  C_  ( RR  ^m  ( 1 ... N
) ) )  ->  I  =  U. ( Rt  I ) )
191182, 186, 190mp2an 676 . . . . . . 7  |-  I  = 
U. ( Rt  I )
192191bwth 20412 . . . . . 6  |-  ( ( ( Rt  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 `  ( Rt  I ) ) `  ran  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) ) )
1931923expia 1207 . . . . 5  |-  ( ( ( Rt  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 `  ( Rt  I ) ) `  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) ) ) )
194175, 58, 193sylancr 667 . . . 4  |-  ( ph  ->  ( -.  ran  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  e.  Fin  ->  E. c  e.  I  c  e.  ( ( limPt `  ( Rt  I ) ) `  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) ) ) )
195 cmptop 20397 . . . . . . . . 9  |-  ( ( Rt  I )  e.  Comp  -> 
( Rt  I )  e.  Top )
196175, 195ax-mp 5 . . . . . . . 8  |-  ( Rt  I )  e.  Top
197191islp3 20149 . . . . . . . 8  |-  ( ( ( Rt  I )  e.  Top  /\ 
ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) )  C_  I  /\  c  e.  I
)  ->  ( c  e.  ( ( limPt `  ( Rt  I ) ) `  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) )  <->  A. v  e.  ( Rt  I ) ( c  e.  v  ->  (
v  i^i  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  \  { c } ) )  =/=  (/) ) ) )
198196, 197mp3an1 1347 . . . . . . 7  |-  ( ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) )  C_  I  /\  c  e.  I
)  ->  ( c  e.  ( ( limPt `  ( Rt  I ) ) `  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) )  <->  A. v  e.  ( Rt  I ) ( c  e.  v  ->  (
v  i^i  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  \  { c } ) )  =/=  (/) ) ) )
19958, 198sylan 473 . . . . . 6  |-  ( (
ph  /\  c  e.  I )  ->  (
c  e.  ( (
limPt `  ( Rt  I ) ) `  ran  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) )  <->  A. v  e.  ( Rt  I ) ( c  e.  v  ->  (
v  i^i  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  \  { c } ) )  =/=  (/) ) ) )
200 fzfid 12186 . . . . . . . . . . . . 13  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  ( 1 ... N
)  e.  Fin )
201155a1i 11 . . . . . . . . . . . . 13  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) : ( 1 ... N ) --> Top )
202 nnrecre 10647 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  NN  ->  (
1  /  i )  e.  RR )
203202rexrd 9691 . . . . . . . . . . . . . . . 16  |-  ( i  e.  NN  ->  (
1  /  i )  e.  RR* )
204 eqid 2422 . . . . . . . . . . . . . . . . . . 19  |-  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )
205135, 204tgioo 21801 . . . . . . . . . . . . . . . . . 18  |-  ( topGen ` 
ran  (,) )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( RR  X.  RR ) ) )
206205blopn 21502 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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  (,) ) )
207136, 206mp3an1 1347 . . . . . . . . . . . . . . . 16  |-  ( ( ( c `  m
)  e.  RR  /\  ( 1  /  i
)  e.  RR* )  ->  ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) )  e.  ( topGen `  ran  (,) )
)
208132, 203, 207syl2an 479 . . . . . . . . . . . . . . 15  |-  ( ( ( c  e.  I  /\  m  e.  (
1 ... N ) )  /\  i  e.  NN )  ->  ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  e.  ( topGen ` 
ran  (,) ) )
209208an32s 811 . . . . . . . . . . . . . 14  |-  ( ( ( c  e.  I  /\  i  e.  NN )  /\  m  e.  ( 1 ... N ) )  ->  ( (
c `  m )
( ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  e.  ( topGen ` 
ran  (,) ) )
210160fvconst2 6132 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( 1 ... N )  ->  (
( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  m
)  =  ( topGen ` 
ran  (,) ) )
211210adantl 467 . . . . . . . . . . . . . 14  |-  ( ( ( c  e.  I  /\  i  e.  NN )  /\  m  e.  ( 1 ... N ) )  ->  ( (
( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) `  m
)  =  ( topGen ` 
ran  (,) ) )
212209, 211eleqtrrd 2513 . . . . . . . . . . . . 13  |-  ( ( ( 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
) )
213 noel 3765 . . . . . . . . . . . . . . . 16  |-  -.  m  e.  (/)
214 difid 3863 . . . . . . . . . . . . . . . . 17  |-  ( ( 1 ... N ) 
\  ( 1 ... N ) )  =  (/)
215214eleq2i 2500 . . . . . . . . . . . . . . . 16  |-  ( m  e.  ( ( 1 ... N )  \ 
( 1 ... N
) )  <->  m  e.  (/) )
216213, 215mtbir 300 . . . . . . . . . . . . . . 15  |-  -.  m  e.  ( ( 1 ... N )  \  (
1 ... N ) )
217216pm2.21i 134 . . . . . . . . . . . . . 14  |-  ( m  e.  ( ( 1 ... N )  \ 
( 1 ... N
) )  ->  (
( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  =  U. (
( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  m
) )
218217adantl 467 . . . . . . . . . . . . 13  |-  ( ( ( 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
) )
219200, 201, 200, 212, 218ptopn 20585 . . . . . . . . . . . 12  |-  ( ( 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  (,) ) } ) ) )
220219, 149syl6eleqr 2521 . . . . . . . . . . 11  |-  ( ( c  e.  I  /\  i  e.  NN )  -> 
X_ m  e.  ( 1 ... N ) ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) )  e.  R )
221 ovex 6330 . . . . . . . . . . . . 13  |-  ( ( 0 [,] 1 )  ^m  ( 1 ... N ) )  e. 
_V
22248, 221eqeltri 2506 . . . . . . . . . . . 12  |-  I  e. 
_V
223 elrestr 15315 . . . . . . . . . . . 12  |-  ( ( 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.  ( Rt  I ) )
224180, 222, 223mp3an12 1350 . . . . . . . . . . 11  |-  ( 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.  ( Rt  I ) )
225220, 224syl 17 . . . . . . . . . 10  |-  ( ( 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.  ( Rt  I ) )
226 difss 3592 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) )
227 imassrn 5195 . . . . . . . . . . . . 13  |-  ( ( 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 } ) ) )
228226, 227sstri 3473 . . . . . . . . . . . 12  |-  ( ( ( 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 } ) ) )
229228, 58syl5ss 3475 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )
" ( 1..^ i ) )  \  {
c } )  C_  I )
230 haust1 20355 . . . . . . . . . . . . . 14  |-  ( R  e.  Haus  ->  R  e. 
Fre )
231180, 230ax-mp 5 . . . . . . . . . . . . 13  |-  R  e. 
Fre
232 restt1 20370 . . . . . . . . . . . . 13  |-  ( ( R  e.  Fre  /\  I  e.  _V )  ->  ( Rt  I )  e.  Fre )
233231, 222, 232mp2an 676 . . . . . . . . . . . 12  |-  ( Rt  I )  e.  Fre
234 funmpt 5634 . . . . . . . . . . . . . 14  |-  Fun  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )
235 imafi 7870 . . . . . . . . . . . . . 14  |-  ( ( 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 )
236234, 114, 235mp2an 676 . . . . . . . . . . . . 13  |-  ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  e. 
Fin
237 diffi 7806 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
238236, 237ax-mp 5 . . . . . . . . . . . 12  |-  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } )  e.  Fin
239191t1ficld 20330 . . . . . . . . . . . 12  |-  ( ( ( Rt  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 `  ( Rt  I ) ) )
240233, 238, 239mp3an13 1351 . . . . . . . . . . 11  |-  ( ( ( ( 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 `  ( Rt  I ) ) )
241229, 240syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )
" ( 1..^ i ) )  \  {
c } )  e.  ( Clsd `  ( Rt  I ) ) )
242191difopn 20036 . . . . . . . . . 10  |-  ( ( ( X_ m  e.  ( 1 ... N
) ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I )  e.  ( Rt  I )  /\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } )  e.  ( Clsd `  ( Rt  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.  ( Rt  I ) )
243225, 241, 242syl2anr 480 . . . . . . . . 9  |-  ( (
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.  ( Rt  I ) )
244243anassrs 652 . . . . . . . 8  |-  ( ( ( 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.  ( Rt  I ) )
245 eleq2 2495 . . . . . . . . . . 11  |-  ( 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 } ) ) ) )
246 ineq1 3657 . . . . . . . . . . . 12  |-  ( 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 } ) ) )
247246neeq1d 2701 . . . . . . . . . . 11  |-  ( 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 } ) )  =/=  (/) ) )
248245, 247imbi12d 321 . . . . . . . . . 10  |-  ( 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 } ) )  =/=  (/) ) ) )
249248rspcva 3180 . . . . . . . . 9  |-  ( ( ( ( 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.  ( Rt  I )  /\  A. v  e.  ( Rt  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 } ) )  =/=  (/) ) )
250 ffn 5743 . . . . . . . . . . . . . . . 16  |-  ( c : ( 1 ... N ) --> ( 0 [,] 1 )  -> 
c  Fn  ( 1 ... N ) )
251130, 250syl 17 . . . . . . . . . . . . . . 15  |-  ( c  e.  I  ->  c  Fn  ( 1 ... N
) )
252251adantr 466 . . . . . . . . . . . . . 14  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  c  Fn  ( 1 ... N ) )
253140ralrimiva 2839 . . . . . . . . . . . . . 14  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  A. m  e.  ( 1 ... N ) ( c `  m
)  e.  ( ( c `  m ) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) ) )
254106elixp 7534 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) )
255252, 253, 254sylanbrc 668 . . . . . . . . . . . . 13  |-  ( ( 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 458 . . . . . . . . . . . . 13  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  c  e.  I )
257255, 256elind 3650 . . . . . . . . . . . 12  |-  ( ( 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 4125 . . . . . . . . . . . 12  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  -.  c  e.  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " (
1..^ i ) ) 
\  { c } ) )
259257, 258eldifd 3447 . . . . . . . . . . 11  |-  ( ( 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 } ) ) )
260259adantll 718 . . . . . . . . . 10  |-  ( ( ( 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 760 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) )
262261anim1i 570 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 458 . . . . . . . . . . . . . . . 16  |-  ( ( 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 } ) ) ) )
264262, 263anim12i 568 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( 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 3649 . . . . . . . . . . . . . . . 16  |-  ( 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 876 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( 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.  ( (