Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem35 Unicode version

Theorem stoweidlem35 27784
Description: This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p(t_0) = 0, and p > 0 on T - U. Here  ( q `  i ) is used to represent p(t_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem35.1  |-  F/ t
ph
stoweidlem35.2  |-  F/ w ph
stoweidlem35.3  |-  F/ h ph
stoweidlem35.4  |-  Q  =  { h  e.  A  |  ( ( h `
 Z )  =  0  /\  A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 ) ) }
stoweidlem35.5  |-  W  =  { w  e.  J  |  E. h  e.  Q  w  =  { t  e.  T  |  0  <  ( h `  t
) } }
stoweidlem35.6  |-  G  =  ( w  e.  X  |->  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
stoweidlem35.7  |-  ( ph  ->  A  e.  _V )
stoweidlem35.8  |-  ( ph  ->  X  e.  Fin )
stoweidlem35.9  |-  ( ph  ->  X  C_  W )
stoweidlem35.10  |-  ( ph  ->  ( T  \  U
)  C_  U. X )
stoweidlem35.11  |-  ( ph  ->  ( T  \  U
)  =/=  (/) )
Assertion
Ref Expression
stoweidlem35  |-  ( ph  ->  E. m E. q
( m  e.  NN  /\  ( q : ( 1 ... m ) --> Q  /\  A. t  e.  ( T  \  U
) E. i  e.  ( 1 ... m
) 0  <  (
( q `  i
) `  t )
) ) )
Distinct variable groups:    h, i,
t, w    i, m, q, t    i, G    w, Q    T, h, w    U, q    ph, i, m    A, h, t    h, X, i, t, w    w, m   
m, G    Q, q    T, q    t, Z    w, U
Allowed substitution hints:    ph( w, t, h, q)    A( w, i, m, q)    Q( t, h, i, m)    T( t, i, m)    U( t, h, i, m)    G( w, t, h, q)    J( w, t, h, i, m, q)    W( w, t, h, i, m, q)    X( m, q)    Z( w, h, i, m, q)

Proof of Theorem stoweidlem35
Dummy variables  f 
g  k  l are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem35.8 . . . . . . . . . . . . 13  |-  ( ph  ->  X  e.  Fin )
2 stoweidlem35.6 . . . . . . . . . . . . . . 15  |-  G  =  ( w  e.  X  |->  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
3 mptfi 7155 . . . . . . . . . . . . . . 15  |-  ( X  e.  Fin  ->  (
w  e.  X  |->  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  ( h `  t
) } } )  e.  Fin )
42, 3syl5eqel 2367 . . . . . . . . . . . . . 14  |-  ( X  e.  Fin  ->  G  e.  Fin )
5 rnfi 7141 . . . . . . . . . . . . . 14  |-  ( G  e.  Fin  ->  ran  G  e.  Fin )
64, 5syl 15 . . . . . . . . . . . . 13  |-  ( X  e.  Fin  ->  ran  G  e.  Fin )
71, 6syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ran  G  e.  Fin )
87ancli 534 . . . . . . . . . . 11  |-  ( ph  ->  ( ph  /\  ran  G  e.  Fin ) )
9 fnchoice 27700 . . . . . . . . . . . . 13  |-  ( ran 
G  e.  Fin  ->  E. g ( g  Fn 
ran  G  /\  A. l  e.  ran  G ( l  =/=  (/)  ->  ( g `  l )  e.  l ) ) )
109adantl 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ran  G  e. 
Fin )  ->  E. g
( g  Fn  ran  G  /\  A. l  e. 
ran  G ( l  =/=  (/)  ->  ( g `  l )  e.  l ) ) )
11 simprl 732 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( g  Fn  ran  G  /\  A. l  e.  ran  G ( l  =/=  (/)  ->  (
g `  l )  e.  l ) ) )  ->  g  Fn  ran  G )
12 simpll 730 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
g  Fn  ran  G  /\  A. l  e.  ran  G ( l  =/=  (/)  ->  (
g `  l )  e.  l ) ) )  /\  k  e.  ran  G )  ->  ph )
13 simpr 447 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
g  Fn  ran  G  /\  A. l  e.  ran  G ( l  =/=  (/)  ->  (
g `  l )  e.  l ) ) )  /\  k  e.  ran  G )  ->  k  e.  ran  G )
1412, 13jca 518 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
g  Fn  ran  G  /\  A. l  e.  ran  G ( l  =/=  (/)  ->  (
g `  l )  e.  l ) ) )  /\  k  e.  ran  G )  ->  ( ph  /\  k  e.  ran  G
) )
152elrnmpt 4926 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  ran  G  -> 
( k  e.  ran  G  <->  E. w  e.  X  k  =  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } } ) )
1615ibi 232 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  ran  G  ->  E. w  e.  X  k  =  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } } )
1716adantl 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  k  e.  ran  G )  ->  E. w  e.  X  k  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
18 stoweidlem35.2 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ w ph
19 nfcv 2419 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ w
k
20 nfmpt1 4109 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  F/_ w
( w  e.  X  |->  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
212, 20nfcxfr 2416 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/_ w G
2221nfrn 4921 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ w ran  G
2319, 22nfel 2427 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ w  k  e.  ran  G
2418, 23nfan 1771 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ w
( ph  /\  k  e.  ran  G )
25 simplll 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  k  e.  ran  G )  /\  w  e.  X
)  /\  k  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)  ->  ph )
26 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  k  e.  ran  G )  /\  w  e.  X
)  /\  k  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)  ->  w  e.  X )
2725, 26jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  k  e.  ran  G )  /\  w  e.  X
)  /\  k  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)  ->  ( ph  /\  w  e.  X ) )
28 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  k  e.  ran  G )  /\  w  e.  X
)  /\  k  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)  ->  k  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
2927, 28jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  k  e.  ran  G )  /\  w  e.  X
)  /\  k  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)  ->  ( ( ph  /\  w  e.  X
)  /\  k  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
) )
30 stoweidlem35.9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  X  C_  W )
3130sselda 3180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  w  e.  X )  ->  w  e.  W )
32 stoweidlem35.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  W  =  { w  e.  J  |  E. h  e.  Q  w  =  { t  e.  T  |  0  <  ( h `  t
) } }
3332eleq2i 2347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( w  e.  W  <->  w  e.  { w  e.  J  |  E. h  e.  Q  w  =  { t  e.  T  |  0  <  ( h `  t
) } } )
3431, 33sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  w  e.  X )  ->  w  e.  { w  e.  J  |  E. h  e.  Q  w  =  { t  e.  T  |  0  <  ( h `  t
) } } )
35 rabid 2716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w  e.  { w  e.  J  |  E. h  e.  Q  w  =  { t  e.  T  |  0  <  (
h `  t ) } }  <->  ( w  e.  J  /\  E. h  e.  Q  w  =  { t  e.  T  |  0  <  (
h `  t ) } ) )
3634, 35sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  w  e.  X )  ->  (
w  e.  J  /\  E. h  e.  Q  w  =  { t  e.  T  |  0  < 
( h `  t
) } ) )
3736simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  w  e.  X )  ->  E. h  e.  Q  w  =  { t  e.  T  |  0  <  (
h `  t ) } )
38 df-rex 2549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. h  e.  Q  w  =  { t  e.  T  |  0  < 
( h `  t
) }  <->  E. h
( h  e.  Q  /\  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } ) )
3937, 38sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  w  e.  X )  ->  E. h
( h  e.  Q  /\  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } ) )
40 rabid 2716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( h  e.  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } }  <->  ( h  e.  Q  /\  w  =  { t  e.  T  |  0  <  (
h `  t ) } ) )
4140exbii 1569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. h  h  e.  {
h  e.  Q  |  w  =  { t  e.  T  |  0  <  ( h `  t
) } }  <->  E. h
( h  e.  Q  /\  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } ) )
4241biimpri 197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( E. h ( h  e.  Q  /\  w  =  { t  e.  T  |  0  <  (
h `  t ) } )  ->  E. h  h  e.  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } } )
4339, 42syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  w  e.  X )  ->  E. h  h  e.  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } } )
4443adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  w  e.  X )  /\  k  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)  ->  E. h  h  e.  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } } )
45 stoweidlem35.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  F/ h ph
46 nfv 1605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  F/ h  w  e.  X
4745, 46nfan 1771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  F/ h
( ph  /\  w  e.  X )
48 nfcv 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  F/_ h
k
49 nfrab1 2720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  F/_ h { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
5048, 49nfeq 2426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  F/ h  k  =  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } }
5147, 50nfan 1771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  F/ h
( ( ph  /\  w  e.  X )  /\  k  =  {
h  e.  Q  |  w  =  { t  e.  T  |  0  <  ( h `  t
) } } )
52 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  w  e.  X )  /\  k  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)  ->  k  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
53 eleq2 2344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  =  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } }  ->  ( h  e.  k  <->  h  e.  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  ( h `  t
) } } ) )
5453biimprd 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( k  =  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } }  ->  ( h  e.  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } }  ->  h  e.  k ) )
5552, 54syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  w  e.  X )  /\  k  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)  ->  ( h  e.  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }  ->  h  e.  k ) )
5651, 55eximd 1750 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  w  e.  X )  /\  k  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)  ->  ( E. h  h  e.  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } }  ->  E. h  h  e.  k )
)
5744, 56mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  w  e.  X )  /\  k  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)  ->  E. h  h  e.  k )
5829, 57syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  k  e.  ran  G )  /\  w  e.  X
)  /\  k  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)  ->  E. h  h  e.  k )
5958ex 423 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  k  e.  ran  G )  /\  w  e.  X )  ->  ( k  =  {
h  e.  Q  |  w  =  { t  e.  T  |  0  <  ( h `  t
) } }  ->  E. h  h  e.  k ) )
6059ex 423 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  k  e.  ran  G )  ->  (
w  e.  X  -> 
( k  =  {
h  e.  Q  |  w  =  { t  e.  T  |  0  <  ( h `  t
) } }  ->  E. h  h  e.  k ) ) )
6124, 60reximdai 2651 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  k  e.  ran  G )  ->  ( E. w  e.  X  k  =  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } }  ->  E. w  e.  X  E. h  h  e.  k )
)
6217, 61mpd 14 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  ran  G )  ->  E. w  e.  X  E. h  h  e.  k )
63 nfv 1605 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ w E. h  h  e.  k
64 idd 21 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  e.  X  ->  ( E. h  h  e.  k  ->  E. h  h  e.  k ) )
6564a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  k  e.  ran  G )  ->  (
w  e.  X  -> 
( E. h  h  e.  k  ->  E. h  h  e.  k )
) )
6624, 63, 65rexlimd 2664 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  ran  G )  ->  ( E. w  e.  X  E. h  h  e.  k  ->  E. h  h  e.  k ) )
6762, 66mpd 14 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  ran  G )  ->  E. h  h  e.  k )
68 n0 3464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =/=  (/)  <->  E. h  h  e.  k )
6967, 68sylibr 203 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  ran  G )  ->  k  =/=  (/) )
7014, 69syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
g  Fn  ran  G  /\  A. l  e.  ran  G ( l  =/=  (/)  ->  (
g `  l )  e.  l ) ) )  /\  k  e.  ran  G )  ->  k  =/=  (/) )
71 simplrr 737 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
g  Fn  ran  G  /\  A. l  e.  ran  G ( l  =/=  (/)  ->  (
g `  l )  e.  l ) ) )  /\  k  e.  ran  G )  ->  A. l  e.  ran  G ( l  =/=  (/)  ->  ( g `  l )  e.  l ) )
7271, 13jca 518 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
g  Fn  ran  G  /\  A. l  e.  ran  G ( l  =/=  (/)  ->  (
g `  l )  e.  l ) ) )  /\  k  e.  ran  G )  ->  ( A. l  e.  ran  G ( l  =/=  (/)  ->  (
g `  l )  e.  l )  /\  k  e.  ran  G ) )
73 neeq1 2454 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( l  =  k  ->  (
l  =/=  (/)  <->  k  =/=  (/) ) )
74 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( l  =  k  ->  (
g `  l )  =  ( g `  k ) )
7574eleq1d 2349 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( l  =  k  ->  (
( g `  l
)  e.  l  <->  ( g `  k )  e.  l ) )
76 eleq2 2344 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( l  =  k  ->  (
( g `  k
)  e.  l  <->  ( g `  k )  e.  k ) )
7775, 76bitrd 244 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( l  =  k  ->  (
( g `  l
)  e.  l  <->  ( g `  k )  e.  k ) )
7873, 77imbi12d 311 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  =  k  ->  (
( l  =/=  (/)  ->  (
g `  l )  e.  l )  <->  ( k  =/=  (/)  ->  ( g `  k )  e.  k ) ) )
7978rspccva 2883 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A. l  e.  ran  G ( l  =/=  (/)  ->  (
g `  l )  e.  l )  /\  k  e.  ran  G )  -> 
( k  =/=  (/)  ->  (
g `  k )  e.  k ) )
8072, 79syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
g  Fn  ran  G  /\  A. l  e.  ran  G ( l  =/=  (/)  ->  (
g `  l )  e.  l ) ) )  /\  k  e.  ran  G )  ->  ( k  =/=  (/)  ->  ( g `  k )  e.  k ) )
8170, 80mpd 14 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
g  Fn  ran  G  /\  A. l  e.  ran  G ( l  =/=  (/)  ->  (
g `  l )  e.  l ) ) )  /\  k  e.  ran  G )  ->  ( g `  k )  e.  k )
8281ralrimiva 2626 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( g  Fn  ran  G  /\  A. l  e.  ran  G ( l  =/=  (/)  ->  (
g `  l )  e.  l ) ) )  ->  A. k  e.  ran  G ( g `  k
)  e.  k )
83 fveq2 5525 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  l  ->  (
g `  k )  =  ( g `  l ) )
8483eleq1d 2349 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  l  ->  (
( g `  k
)  e.  k  <->  ( g `  l )  e.  k ) )
85 eleq2 2344 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  l  ->  (
( g `  l
)  e.  k  <->  ( g `  l )  e.  l ) )
8684, 85bitrd 244 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  l  ->  (
( g `  k
)  e.  k  <->  ( g `  l )  e.  l ) )
8786cbvralv 2764 . . . . . . . . . . . . . . . . 17  |-  ( A. k  e.  ran  G ( g `  k )  e.  k  <->  A. l  e.  ran  G ( g `
 l )  e.  l )
8882, 87sylib 188 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( g  Fn  ran  G  /\  A. l  e.  ran  G ( l  =/=  (/)  ->  (
g `  l )  e.  l ) ) )  ->  A. l  e.  ran  G ( g `  l
)  e.  l )
8911, 88jca 518 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( g  Fn  ran  G  /\  A. l  e.  ran  G ( l  =/=  (/)  ->  (
g `  l )  e.  l ) ) )  ->  ( g  Fn 
ran  G  /\  A. l  e.  ran  G ( g `
 l )  e.  l ) )
9089ex 423 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( g  Fn 
ran  G  /\  A. l  e.  ran  G ( l  =/=  (/)  ->  ( g `  l )  e.  l ) )  ->  (
g  Fn  ran  G  /\  A. l  e.  ran  G ( g `  l
)  e.  l ) ) )
9190adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ran  G  e. 
Fin )  ->  (
( g  Fn  ran  G  /\  A. l  e. 
ran  G ( l  =/=  (/)  ->  ( g `  l )  e.  l ) )  ->  (
g  Fn  ran  G  /\  A. l  e.  ran  G ( g `  l
)  e.  l ) ) )
9291eximdv 1608 . . . . . . . . . . . 12  |-  ( (
ph  /\  ran  G  e. 
Fin )  ->  ( E. g ( g  Fn 
ran  G  /\  A. l  e.  ran  G ( l  =/=  (/)  ->  ( g `  l )  e.  l ) )  ->  E. g
( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l ) ) )
9310, 92mpd 14 . . . . . . . . . . 11  |-  ( (
ph  /\  ran  G  e. 
Fin )  ->  E. g
( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l ) )
948, 93syl 15 . . . . . . . . . 10  |-  ( ph  ->  E. g ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l ) )
9594a1d 22 . . . . . . . . 9  |-  ( ph  ->  ( m  e.  NN  ->  E. g ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l ) ) )
9695ralrimiv 2625 . . . . . . . 8  |-  ( ph  ->  A. m  e.  NN  E. g ( g  Fn 
ran  G  /\  A. l  e.  ran  G ( g `
 l )  e.  l ) )
97 stoweidlem35.10 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( T  \  U
)  C_  U. X )
98 stoweidlem35.11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( T  \  U
)  =/=  (/) )
9997, 98jca 518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( T  \  U )  C_  U. X  /\  ( T  \  U
)  =/=  (/) ) )
100 ssn0 3487 . . . . . . . . . . . . . 14  |-  ( ( ( T  \  U
)  C_  U. X  /\  ( T  \  U )  =/=  (/) )  ->  U. X  =/=  (/) )
10199, 100syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  U. X  =/=  (/) )
102 df-ne 2448 . . . . . . . . . . . . 13  |-  ( U. X  =/=  (/)  <->  -.  U. X  =  (/) )
103101, 102sylib 188 . . . . . . . . . . . 12  |-  ( ph  ->  -.  U. X  =  (/) )
104 unieq 3836 . . . . . . . . . . . . . 14  |-  ( X  =  (/)  ->  U. X  =  U. (/) )
105 uni0 3854 . . . . . . . . . . . . . 14  |-  U. (/)  =  (/)
106104, 105syl6eq 2331 . . . . . . . . . . . . 13  |-  ( X  =  (/)  ->  U. X  =  (/) )
107 con3 126 . . . . . . . . . . . . 13  |-  ( ( X  =  (/)  ->  U. X  =  (/) )  ->  ( -.  U. X  =  (/)  ->  -.  X  =  (/) ) )
108106, 107ax-mp 8 . . . . . . . . . . . 12  |-  ( -. 
U. X  =  (/)  ->  -.  X  =  (/) )
109103, 108syl 15 . . . . . . . . . . 11  |-  ( ph  ->  -.  X  =  (/) )
110 dm0rn0 4895 . . . . . . . . . . . 12  |-  ( dom 
G  =  (/)  <->  ran  G  =  (/) )
111 stoweidlem35.4 . . . . . . . . . . . . . . . . . . . . 21  |-  Q  =  { h  e.  A  |  ( ( h `
 Z )  =  0  /\  A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 ) ) }
112 stoweidlem35.7 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  A  e.  _V )
113 rabexg 4164 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A  e.  _V  ->  { h  e.  A  |  (
( h `  Z
)  =  0  /\ 
A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) ) }  e.  _V )
114112, 113syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  { h  e.  A  |  ( ( h `
 Z )  =  0  /\  A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 ) ) }  e.  _V )
115111, 114syl5eqel 2367 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  Q  e.  _V )
116 nfrab1 2720 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ h { h  e.  A  |  ( ( h `
 Z )  =  0  /\  A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 ) ) }
117111, 116nfcxfr 2416 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ h Q
118117rabexgf 27695 . . . . . . . . . . . . . . . . . . . 20  |-  ( Q  e.  _V  ->  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } }  e.  _V )
119115, 118syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }  e.  _V )
120119adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  w  e.  X )  ->  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } }  e.  _V )
121120ex 423 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( w  e.  X  ->  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }  e.  _V ) )
12218, 121ralrimi 2624 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A. w  e.  X  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }  e.  _V )
1232fmpt 5681 . . . . . . . . . . . . . . . 16  |-  ( A. w  e.  X  {
h  e.  Q  |  w  =  { t  e.  T  |  0  <  ( h `  t
) } }  e.  _V 
<->  G : X --> _V )
124122, 123sylib 188 . . . . . . . . . . . . . . 15  |-  ( ph  ->  G : X --> _V )
125 dffn2 5390 . . . . . . . . . . . . . . 15  |-  ( G  Fn  X  <->  G : X
--> _V )
126124, 125sylibr 203 . . . . . . . . . . . . . 14  |-  ( ph  ->  G  Fn  X )
127 fndm 5343 . . . . . . . . . . . . . 14  |-  ( G  Fn  X  ->  dom  G  =  X )
128126, 127syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  dom  G  =  X )
129128eqeq1d 2291 . . . . . . . . . . . 12  |-  ( ph  ->  ( dom  G  =  (/) 
<->  X  =  (/) ) )
130110, 129syl5bbr 250 . . . . . . . . . . 11  |-  ( ph  ->  ( ran  G  =  (/) 
<->  X  =  (/) ) )
131109, 130mtbird 292 . . . . . . . . . 10  |-  ( ph  ->  -.  ran  G  =  (/) )
132 fz1f1o 12183 . . . . . . . . . . . 12  |-  ( ran 
G  e.  Fin  ->  ( ran  G  =  (/)  \/  ( ( # `  ran  G )  e.  NN  /\  E. f  f : ( 1 ... ( # `  ran  G ) ) -1-1-onto-> ran 
G ) ) )
1337, 132syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( ran  G  =  (/)  \/  ( ( # `  ran  G )  e.  NN  /\  E. f 
f : ( 1 ... ( # `  ran  G ) ) -1-1-onto-> ran  G ) ) )
134 df-or 359 . . . . . . . . . . 11  |-  ( ( ran  G  =  (/)  \/  ( ( # `  ran  G )  e.  NN  /\  E. f  f : ( 1 ... ( # `  ran  G ) ) -1-1-onto-> ran 
G ) )  <->  ( -.  ran  G  =  (/)  ->  (
( # `  ran  G
)  e.  NN  /\  E. f  f : ( 1 ... ( # `  ran  G ) ) -1-1-onto-> ran 
G ) ) )
135133, 134sylib 188 . . . . . . . . . 10  |-  ( ph  ->  ( -.  ran  G  =  (/)  ->  ( ( # `
 ran  G )  e.  NN  /\  E. f 
f : ( 1 ... ( # `  ran  G ) ) -1-1-onto-> ran  G ) ) )
136131, 135mpd 14 . . . . . . . . 9  |-  ( ph  ->  ( ( # `  ran  G )  e.  NN  /\  E. f  f : ( 1 ... ( # `  ran  G ) ) -1-1-onto-> ran 
G ) )
137 oveq2 5866 . . . . . . . . . . . 12  |-  ( m  =  ( # `  ran  G )  ->  ( 1 ... m )  =  ( 1 ... ( # `
 ran  G )
) )
138 f1oeq2 5464 . . . . . . . . . . . 12  |-  ( ( 1 ... m )  =  ( 1 ... ( # `  ran  G ) )  ->  (
f : ( 1 ... m ) -1-1-onto-> ran  G  <->  f : ( 1 ... ( # `  ran  G ) ) -1-1-onto-> ran  G ) )
139137, 138syl 15 . . . . . . . . . . 11  |-  ( m  =  ( # `  ran  G )  ->  ( f : ( 1 ... m ) -1-1-onto-> ran  G  <->  f :
( 1 ... ( # `
 ran  G )
)
-1-1-onto-> ran  G ) )
140139exbidv 1612 . . . . . . . . . 10  |-  ( m  =  ( # `  ran  G )  ->  ( E. f  f : ( 1 ... m ) -1-1-onto-> ran 
G  <->  E. f  f : ( 1 ... ( # `
 ran  G )
)
-1-1-onto-> ran  G ) )
141140rspcev 2884 . . . . . . . . 9  |-  ( ( ( # `  ran  G )  e.  NN  /\  E. f  f : ( 1 ... ( # `  ran  G ) ) -1-1-onto-> ran 
G )  ->  E. m  e.  NN  E. f  f : ( 1 ... m ) -1-1-onto-> ran  G )
142136, 141syl 15 . . . . . . . 8  |-  ( ph  ->  E. m  e.  NN  E. f  f : ( 1 ... m ) -1-1-onto-> ran 
G )
14396, 142jca 518 . . . . . . 7  |-  ( ph  ->  ( A. m  e.  NN  E. g ( g  Fn  ran  G  /\  A. l  e.  ran  G ( g `  l
)  e.  l )  /\  E. m  e.  NN  E. f  f : ( 1 ... m ) -1-1-onto-> ran  G ) )
144 r19.29 2683 . . . . . . 7  |-  ( ( A. m  e.  NN  E. g ( g  Fn 
ran  G  /\  A. l  e.  ran  G ( g `
 l )  e.  l )  /\  E. m  e.  NN  E. f 
f : ( 1 ... m ) -1-1-onto-> ran  G
)  ->  E. m  e.  NN  ( E. g
( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l )  /\  E. f  f : ( 1 ... m ) -1-1-onto-> ran 
G ) )
145143, 144syl 15 . . . . . 6  |-  ( ph  ->  E. m  e.  NN  ( E. g ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l )  /\  E. f  f : ( 1 ... m ) -1-1-onto-> ran  G ) )
146 eeanv 1854 . . . . . . . . 9  |-  ( E. g E. f ( ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran  G )  <->  ( E. g ( g  Fn 
ran  G  /\  A. l  e.  ran  G ( g `
 l )  e.  l )  /\  E. f  f : ( 1 ... m ) -1-1-onto-> ran 
G ) )
147146biimpri 197 . . . . . . . 8  |-  ( ( E. g ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l )  /\  E. f  f : ( 1 ... m ) -1-1-onto-> ran  G )  ->  E. g E. f ( ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) )
148147a1i 10 . . . . . . 7  |-  ( ph  ->  ( ( E. g
( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l )  /\  E. f  f : ( 1 ... m ) -1-1-onto-> ran 
G )  ->  E. g E. f ( ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran 
G ) ) )
149148reximdv 2654 . . . . . 6  |-  ( ph  ->  ( E. m  e.  NN  ( E. g
( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l )  /\  E. f  f : ( 1 ... m ) -1-1-onto-> ran 
G )  ->  E. m  e.  NN  E. g E. f ( ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran 
G ) ) )
150145, 149mpd 14 . . . . 5  |-  ( ph  ->  E. m  e.  NN  E. g E. f ( ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) )
151 df-rex 2549 . . . . 5  |-  ( E. m  e.  NN  E. g E. f ( ( g  Fn  ran  G  /\  A. l  e.  ran  G ( g `  l
)  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran 
G )  <->  E. m
( m  e.  NN  /\ 
E. g E. f
( ( g  Fn 
ran  G  /\  A. l  e.  ran  G ( g `
 l )  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) ) )
152150, 151sylib 188 . . . 4  |-  ( ph  ->  E. m ( m  e.  NN  /\  E. g E. f ( ( g  Fn  ran  G  /\  A. l  e.  ran  G ( g `  l
)  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran 
G ) ) )
153 ax-17 1603 . . . . . . . . . 10  |-  ( m  e.  NN  ->  A. g  m  e.  NN )
154153anim1i 551 . . . . . . . . 9  |-  ( ( m  e.  NN  /\  E. g E. f ( ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) )  ->  ( A. g  m  e.  NN  /\  E. g E. f ( ( g  Fn  ran  G  /\  A. l  e.  ran  G ( g `  l
)  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran 
G ) ) )
155 19.29 1583 . . . . . . . . 9  |-  ( ( A. g  m  e.  NN  /\  E. g E. f ( ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran 
G ) )  ->  E. g ( m  e.  NN  /\  E. f
( ( g  Fn 
ran  G  /\  A. l  e.  ran  G ( g `
 l )  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) ) )
156154, 155syl 15 . . . . . . . 8  |-  ( ( m  e.  NN  /\  E. g E. f ( ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) )  ->  E. g ( m  e.  NN  /\  E. f ( ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran 
G ) ) )
157 ax-17 1603 . . . . . . . . . . 11  |-  ( m  e.  NN  ->  A. f  m  e.  NN )
158157anim1i 551 . . . . . . . . . 10  |-  ( ( m  e.  NN  /\  E. f ( ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran 
G ) )  -> 
( A. f  m  e.  NN  /\  E. f ( ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran 
G ) ) )
159 19.29 1583 . . . . . . . . . 10  |-  ( ( A. f  m  e.  NN  /\  E. f
( ( g  Fn 
ran  G  /\  A. l  e.  ran  G ( g `
 l )  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) )  ->  E. f ( m  e.  NN  /\  (
( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) ) )
160158, 159syl 15 . . . . . . . . 9  |-  ( ( m  e.  NN  /\  E. f ( ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran 
G ) )  ->  E. f ( m  e.  NN  /\  ( ( g  Fn  ran  G  /\  A. l  e.  ran  G ( g `  l
)  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran 
G ) ) )
161160eximi 1563 . . . . . . . 8  |-  ( E. g ( m  e.  NN  /\  E. f
( ( g  Fn 
ran  G  /\  A. l  e.  ran  G ( g `
 l )  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) )  ->  E. g E. f
( m  e.  NN  /\  ( ( g  Fn 
ran  G  /\  A. l  e.  ran  G ( g `
 l )  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) ) )
162156, 161syl 15 . . . . . . 7  |-  ( ( m  e.  NN  /\  E. g E. f ( ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) )  ->  E. g E. f
( m  e.  NN  /\  ( ( g  Fn 
ran  G  /\  A. l  e.  ran  G ( g `
 l )  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) ) )
163 df-3an 936 . . . . . . . . 9  |-  ( ( g  Fn  ran  G  /\  A. l  e.  ran  G ( g `  l
)  e.  l  /\  f : ( 1 ... m ) -1-1-onto-> ran  G )  <->  ( (
g  Fn  ran  G  /\  A. l  e.  ran  G ( g `  l
)  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran 
G ) )
164163anbi2i 675 . . . . . . . 8  |-  ( ( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l  /\  f : ( 1 ... m
)
-1-1-onto-> ran  G ) )  <->  ( m  e.  NN  /\  ( ( g  Fn  ran  G  /\  A. l  e.  ran  G ( g `  l
)  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran 
G ) ) )
1651642exbii 1570 . . . . . . 7  |-  ( E. g E. f ( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l  /\  f : ( 1 ... m
)
-1-1-onto-> ran  G ) )  <->  E. g E. f ( m  e.  NN  /\  ( ( g  Fn  ran  G  /\  A. l  e.  ran  G ( g `  l
)  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran 
G ) ) )
166162, 165sylibr 203 . . . . . 6  |-  ( ( m  e.  NN  /\  E. g E. f ( ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) )  ->  E. g E. f
( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l  /\  f : ( 1 ... m
)
-1-1-onto-> ran  G ) ) )
167166a1i 10 . . . . 5  |-  ( ph  ->  ( ( m  e.  NN  /\  E. g E. f ( ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran 
G ) )  ->  E. g E. f ( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l  /\  f : ( 1 ... m
)
-1-1-onto-> ran  G ) ) ) )
168167eximdv 1608 . . . 4  |-  ( ph  ->  ( E. m ( m  e.  NN  /\  E. g E. f ( ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l )  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) )  ->  E. m E. g E. f ( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) ) ) )
169152, 168mpd 14 . . 3  |-  ( ph  ->  E. m E. g E. f ( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) ) )
170115adantr 451 . . . . . . 7  |-  ( (
ph  /\  ( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) ) )  ->  Q  e.  _V )
171 simprl 732 . . . . . . 7  |-  ( (
ph  /\  ( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) ) )  ->  m  e.  NN )
172 simprr1 1003 . . . . . . 7  |-  ( (
ph  /\  ( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) ) )  ->  g  Fn  ran  G )
173 elex 2796 . . . . . . . . . 10  |-  ( ran 
G  e.  Fin  ->  ran 
G  e.  _V )
174173a1i 10 . . . . . . . . 9  |-  ( ph  ->  ( ran  G  e. 
Fin  ->  ran  G  e.  _V ) )
1757, 174mpd 14 . . . . . . . 8  |-  ( ph  ->  ran  G  e.  _V )
176175adantr 451 . . . . . . 7  |-  ( (
ph  /\  ( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) ) )  ->  ran  G  e. 
_V )
177 simprr2 1004 . . . . . . . . . 10  |-  ( (
ph  /\  ( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) ) )  ->  A. l  e.  ran  G ( g `
 l )  e.  l )
178177adantr 451 . . . . . . . . 9  |-  ( ( ( ph  /\  (
m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l  /\  f : ( 1 ... m
)
-1-1-onto-> ran  G ) ) )  /\  k  e.  ran  G )  ->  A. l  e.  ran  G ( g `
 l )  e.  l )
179 simpr 447 . . . . . . . . 9  |-  ( ( ( ph  /\  (
m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l  /\  f : ( 1 ... m
)
-1-1-onto-> ran  G ) ) )  /\  k  e.  ran  G )  ->  k  e.  ran  G )
180178, 179jca 518 . . . . . . . 8  |-  ( ( ( ph  /\  (
m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l  /\  f : ( 1 ... m
)
-1-1-onto-> ran  G ) ) )  /\  k  e.  ran  G )  ->  ( A. l  e.  ran  G ( g `  l )  e.  l  /\  k  e.  ran  G ) )
18177rspccva 2883 . . . . . . . 8  |-  ( ( A. l  e.  ran  G ( g `  l
)  e.  l  /\  k  e.  ran  G )  ->  ( g `  k )  e.  k )
182180, 181syl 15 . . . . . . 7  |-  ( ( ( ph  /\  (
m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l  /\  f : ( 1 ... m
)
-1-1-onto-> ran  G ) ) )  /\  k  e.  ran  G )  ->  ( g `  k )  e.  k )
183 simprr3 1005 . . . . . . 7  |-  ( (
ph  /\  ( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) ) )  ->  f :
( 1 ... m
)
-1-1-onto-> ran  G )
18497adantr 451 . . . . . . 7  |-  ( (
ph  /\  ( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) ) )  ->  ( T  \  U )  C_  U. X
)
185 stoweidlem35.1 . . . . . . . 8  |-  F/ t
ph
186 nfv 1605 . . . . . . . . 9  |-  F/ t  m  e.  NN
187 nfcv 2419 . . . . . . . . . . 11  |-  F/_ t
g
188 nfcv 2419 . . . . . . . . . . . . . 14  |-  F/_ t X
189 nfcv 2419 . . . . . . . . . . . . . . . 16  |-  F/_ t
w
190 nfrab1 2720 . . . . . . . . . . . . . . . 16  |-  F/_ t { t  e.  T  |  0  <  (
h `  t ) }
191189, 190nfeq 2426 . . . . . . . . . . . . . . 15  |-  F/ t  w  =  { t  e.  T  |  0  <  ( h `  t ) }
192 nfv 1605 . . . . . . . . . . . . . . . . . 18  |-  F/ t ( h `  Z
)  =  0
193 nfra1 2593 . . . . . . . . . . . . . . . . . 18  |-  F/ t A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )
194192, 193nfan 1771 . . . . . . . . . . . . . . . . 17  |-  F/ t ( ( h `  Z )  =  0  /\  A. t  e.  T  ( 0  <_ 
( h `  t
)  /\  ( h `  t )  <_  1
) )
195 nfcv 2419 . . . . . . . . . . . . . . . . 17  |-  F/_ t A
196194, 195nfrab 2721 . . . . . . . . . . . . . . . 16  |-  F/_ t { h  e.  A  |  ( ( h `
 Z )  =  0  /\  A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 ) ) }
197111, 196nfcxfr 2416 . . . . . . . . . . . . . . 15  |-  F/_ t Q
198191, 197nfrab 2721 . . . . . . . . . . . . . 14  |-  F/_ t { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
199188, 198nfmpt 4108 . . . . . . . . . . . . 13  |-  F/_ t
( w  e.  X  |->  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
2002, 199nfcxfr 2416 . . . . . . . . . . . 12  |-  F/_ t G
201200nfrn 4921 . . . . . . . . . . 11  |-  F/_ t ran  G
202187, 201nffn 5340 . . . . . . . . . 10  |-  F/ t  g  Fn  ran  G
203 nfv 1605 . . . . . . . . . . 11  |-  F/ t ( g `  l
)  e.  l
204201, 203nfral 2596 . . . . . . . . . 10  |-  F/ t A. l  e.  ran  G ( g `  l
)  e.  l
205 nfcv 2419 . . . . . . . . . . 11  |-  F/_ t
f
206 nfcv 2419 . . . . . . . . . . 11  |-  F/_ t
( 1 ... m
)
207205, 206, 201nff1o 5470 . . . . . . . . . 10  |-  F/ t  f : ( 1 ... m ) -1-1-onto-> ran  G
208202, 204, 207nf3an 1774 . . . . . . . . 9  |-  F/ t ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l  /\  f : ( 1 ... m
)
-1-1-onto-> ran  G )
209186, 208nfan 1771 . . . . . . . 8  |-  F/ t ( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l  /\  f : ( 1 ... m
)
-1-1-onto-> ran  G ) )
210185, 209nfan 1771 . . . . . . 7  |-  F/ t ( ph  /\  (
m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l  /\  f : ( 1 ... m
)
-1-1-onto-> ran  G ) ) )
211 nfv 1605 . . . . . . . . 9  |-  F/ w  m  e.  NN
212 nfcv 2419 . . . . . . . . . . 11  |-  F/_ w
g
213212, 22nffn 5340 . . . . . . . . . 10  |-  F/ w  g  Fn  ran  G
214 nfv 1605 . . . . . . . . . . 11  |-  F/ w
( g `  l
)  e.  l
21522, 214nfral 2596 . . . . . . . . . 10  |-  F/ w A. l  e.  ran  G ( g `  l
)  e.  l
216 nfcv 2419 . . . . . . . . . . 11  |-  F/_ w
f
217 nfcv 2419 . . . . . . . . . . 11  |-  F/_ w
( 1 ... m
)
218216, 217, 22nff1o 5470 . . . . . . . . . 10  |-  F/ w  f : ( 1 ... m ) -1-1-onto-> ran  G
219213, 215, 218nf3an 1774 . . . . . . . . 9  |-  F/ w
( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l  /\  f : ( 1 ... m
)
-1-1-onto-> ran  G )
220211, 219nfan 1771 . . . . . . . 8  |-  F/ w
( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l  /\  f : ( 1 ... m
)
-1-1-onto-> ran  G ) )
22118, 220nfan 1771 . . . . . . 7  |-  F/ w
( ph  /\  (
m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e. 
ran  G ( g `
 l )  e.  l  /\  f : ( 1 ... m
)
-1-1-onto-> ran  G ) ) )
2222, 170, 171, 172, 176, 182, 183, 184, 210, 221, 117stoweidlem27 27776 . . . . . 6  |-  ( (
ph  /\  ( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) ) )  ->  E. q
( m  e.  NN  /\  ( q : ( 1 ... m ) --> Q  /\  A. t  e.  ( T  \  U
) E. i  e.  ( 1 ... m
) 0  <  (
( q `  i
) `  t )
) ) )
223222ex 423 . . . . 5  |-  ( ph  ->  ( ( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) )  ->  E. q ( m  e.  NN  /\  (
q : ( 1 ... m ) --> Q  /\  A. t  e.  ( T  \  U
) E. i  e.  ( 1 ... m
) 0  <  (
( q `  i
) `  t )
) ) ) )
2242232eximdv 1610 . . . 4  |-  ( ph  ->  ( E. g E. f ( m  e.  NN  /\  ( g  Fn  ran  G  /\  A. l  e.  ran  G
( g `  l
)  e.  l  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) )  ->  E. g E. f E. q ( m  e.  NN  /\  ( q : ( 1 ... m ) --> Q  /\  A. t  e.  ( T 
\  U ) E. i  e.  ( 1 ... m ) 0  <  ( ( q `
 i ) `  t ) ) ) ) )
225224eximdv 1608 . . 3  |-  ( ph  ->  ( E. m E. g E. f ( m  e.  NN  /\  (
g  Fn  ran  G  /\  A. l  e.  ran  G ( g `  l
)  e.  l  /\  f : ( 1 ... m ) -1-1-onto-> ran  G ) )  ->  E. m E. g E. f E. q ( m  e.  NN  /\  ( q : ( 1 ... m ) --> Q  /\  A. t  e.  ( T  \  U
) E. i  e.  ( 1 ... m
) 0  <  (
( q `  i
) `  t )
) ) ) )
226169, 225mpd 14 . 2  |-  ( ph  ->  E. m E. g E. f E. q ( m  e.  NN  /\  ( q : ( 1 ... m ) --> Q  /\  A. t  e.  ( T  \  U
) E. i  e.  ( 1 ... m
) 0  <  (
( q `  i
) `  t )
) ) )
227 id 19 . . . 4  |-  ( E. q ( m  e.  NN  /\  ( q : ( 1 ... m ) --> Q  /\  A. t  e.  ( T 
\  U ) E. i  e.  ( 1 ... m ) 0  <  ( ( q `
 i ) `  t ) ) )  ->  E. q ( m  e.  NN  /\  (
q : ( 1 ... m ) --> Q  /\  A. t  e.  ( T  \  U
) E. i  e.  ( 1 ... m
) 0  <  (
( q `  i
) `  t )
) ) )
228227exlimivv 1667 . . 3  |-  ( E. g E. f E. q ( m  e.  NN  /\  ( q : ( 1 ... m ) --> Q  /\  A. t  e.  ( T 
\  U ) E. i  e.  ( 1 ... m ) 0  <  ( ( q `
 i ) `  t ) ) )  ->  E. q ( m  e.  NN  /\  (
q : ( 1 ... m ) --> Q  /\  A. t  e.  ( T  \  U
) E. i  e.  ( 1 ... m
) 0  <  (
( q `  i
) `  t )
) ) )
229228eximi 1563 . 2  |-  ( E. m E. g E. f E. q ( m  e.  NN  /\  ( q : ( 1 ... m ) --> Q  /\  A. t  e.  ( T  \  U
) E. i  e.  ( 1 ... m
) 0  <  (
( q `  i
) `  t )
) )  ->  E. m E. q ( m  e.  NN  /\  ( q : ( 1 ... m ) --> Q  /\  A. t  e.  ( T 
\  U ) E. i  e.  ( 1 ... m ) 0  <  ( ( q `
 i ) `  t ) ) ) )
230226, 229syl 15 1  |-  ( ph  ->  E. m E. q
( m  e.  NN  /\  ( q : ( 1 ... m ) --> Q  /\  A. t  e.  ( T  \  U
) E. i  e.  ( 1 ... m
) 0  <  (
( q `  i
) `  t )
) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    /\ w3a 934   A.wal 1527   E.wex 1528   F/wnf 1531    = wceq 1623    e. wcel 1684    =/= wne 2446   A.wral 2543   E.wrex 2544   {crab 2547   _Vcvv 2788    \ cdif 3149    C_ wss 3152   (/)c0 3455   U.cuni 3827   class class class wbr 4023    e. cmpt 4077   dom cdm 4689   ran crn 4690    Fn wfn 5250   -->wf 5251   -1-1-onto->wf1o 5254   ` cfv 5255  (class class class)co 5858   Fincfn 6863   0cc0 8737   1c1 8738    < clt 8867    <_ cle 8868   NNcn 9746   ...cfz 10782   #chash 11337
This theorem is referenced by:  stoweidlem53  27802
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-1o 6479  df-oadd 6483  df-er 6660  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867  df-card 7572  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-nn 9747  df-n0 9966  df-z 10025  df-uz 10231  df-fz 10783  df-hash 11338
  Copyright terms: Public domain W3C validator