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

Theorem stoweidlem35 27887
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 7171 . . . . . . . . . . . . . . 15  |-  ( X  e.  Fin  ->  (
w  e.  X  |->  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  ( h `  t
) } } )  e.  Fin )
42, 3syl5eqel 2380 . . . . . . . . . . . . . 14  |-  ( X  e.  Fin  ->  G  e.  Fin )
5 rnfi 7157 . . . . . . . . . . . . . 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 27803 . . . . . . . . . . . . 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 4942 . . . . . . . . . . . . . . . . . . . . . . . . 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 2432 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ w
k
20 nfmpt1 4125 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  F/_ w
( w  e.  X  |->  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
212, 20nfcxfr 2429 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/_ w G
2221nfrn 4937 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ w ran  G
2319, 22nfel 2440 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ w  k  e.  ran  G
2418, 23nfan 1783 . . . . . . . . . . . . . . . . . . . . . . . 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 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2562 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( h  e.  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } }  <->  ( h  e.  Q  /\  w  =  { t  e.  T  |  0  <  (
h `  t ) } ) )
4140exbii 1572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  F/ h  w  e.  X
4745, 46nfan 1783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  F/ h
( ph  /\  w  e.  X )
48 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  F/_ h
k
49 nfrab1 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  F/_ h { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
5048, 49nfeq 2439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  F/ h  k  =  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } }
5147, 50nfan 1783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1762 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2664 . . . . . . . . . . . . . . . . . . . . . . 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 1609 . . . . . . . . . . . . . . . . . . . . . . 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 2677 . . . . . . . . . . . . . . . . . . . . . 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 3477 . . . . . . . . . . . . . . . . . . . . 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 2467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( l  =  k  ->  (
l  =/=  (/)  <->  k  =/=  (/) ) )
74 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( l  =  k  ->  (
g `  l )  =  ( g `  k ) )
7574eleq1d 2362 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( l  =  k  ->  (
( g `  l
)  e.  l  <->  ( g `  k )  e.  l ) )
76 eleq2 2357 . . . . . . . . . . . . . . . . . . . . . . 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 2896 . . . . . . . . . . . . . . . . . . . 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 2639 . . . . . . . . . . . . . . . . 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 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  l  ->  (
g `  k )  =  ( g `  l ) )
8483eleq1d 2362 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  l  ->  (
( g `  k
)  e.  k  <->  ( g `  l )  e.  k ) )
85 eleq2 2357 . . . . . . . . . . . . . . . . . . 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 2777 . . . . . . . . . . . . . . . . 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 1612 . . . . . . . . . . . 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 2638 . . . . . . . 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 3500 . . . . . . . . . . . . . 14  |-  ( ( ( T  \  U
)  C_  U. X  /\  ( T  \  U )  =/=  (/) )  ->  U. X  =/=  (/) )
10199, 100syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  U. X  =/=  (/) )
102 df-ne 2461 . . . . . . . . . . . . 13  |-  ( U. X  =/=  (/)  <->  -.  U. X  =  (/) )
103101, 102sylib 188 . . . . . . . . . . . 12  |-  ( ph  ->  -.  U. X  =  (/) )
104 unieq 3852 . . . . . . . . . . . . . 14  |-  ( X  =  (/)  ->  U. X  =  U. (/) )
105 uni0 3870 . . . . . . . . . . . . . 14  |-  U. (/)  =  (/)
106104, 105syl6eq 2344 . . . . . . . . . . . . 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 4911 . . . . . . . . . . . 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 4180 . . . . . . . . . . . . . . . . . . . . . 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 2380 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  Q  e.  _V )
116 nfrab1 2733 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ h { h  e.  A  |  ( ( h `
 Z )  =  0  /\  A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 ) ) }
117111, 116nfcxfr 2429 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ h Q
118117rabexgf 27798 . . . . . . . . . . . . . . . . . . . 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 2637 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A. w  e.  X  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }  e.  _V )
1232fmpt 5697 . . . . . . . . . . . . . . . 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 5406 . . . . . . . . . . . . . . 15  |-  ( G  Fn  X  <->  G : X
--> _V )
126124, 125sylibr 203 . . . . . . . . . . . . . 14  |-  ( ph  ->  G  Fn  X )
127 fndm 5359 . . . . . . . . . . . . . 14  |-  ( G  Fn  X  ->  dom  G  =  X )
128126, 127syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  dom  G  =  X )
129128eqeq1d 2304 . . . . . . . . . . . 12  |-  ( ph  ->  ( dom  G  =  (/) 
<->  X  =  (/) ) )
130110, 129syl5bbr 250 . . . . . . . . . . 11  |-  ( ph  ->  ( ran  G  =  (/) 
<->  X  =  (/) ) )
131109, 130mtbird 292 . . . . . . . . . 10  |-  ( ph  ->  -.  ran  G  =  (/) )
132 fz1f1o 12199 . . . . . . . . . . . 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 5882 . . . . . . . . . . . 12  |-  ( m  =  ( # `  ran  G )  ->  ( 1 ... m )  =  ( 1 ... ( # `
 ran  G )
) )
138 f1oeq2 5480 . . . . . . . . . . . 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 1616 . . . . . . . . . 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 2897 . . . . . . . . 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 2696 . . . . . . 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 1866 . . . . . . . . 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 2667 . . . . . 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 2562 . . . . 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 1606 . . . . . . . . . 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 1586 . . . . . . . . 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 1606 . . . . . . . . . . 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 1586 . . . . . . . . . 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 1566 . . . . . . . 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 1573 . . . . . . 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 1612 . . . 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 2809 . . . . . . . . . 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 2896 . . . . . . . 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 1609 . . . . . . . . 9  |-  F/ t  m  e.  NN
187 nfcv 2432 . . . . . . . . . . 11  |-  F/_ t
g
188 nfcv 2432 . . . . . . . . . . . . . 14  |-  F/_ t X
189 nfcv 2432 . . . . . . . . . . . . . . . 16  |-  F/_ t
w
190 nfrab1 2733 . . . . . . . . . . . . . . . 16  |-  F/_ t { t  e.  T  |  0  <  (
h `  t ) }
191189, 190nfeq 2439 . . . . . . . . . . . . . . 15  |-  F/ t  w  =  { t  e.  T  |  0  <  ( h `  t ) }
192 nfv 1609 . . . . . . . . . . . . . . . . . 18  |-  F/ t ( h `  Z
)  =  0
193 nfra1 2606 . . . . . . . . . . . . . . . . . 18  |-  F/ t A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )
194192, 193nfan 1783 . . . . . . . . . . . . . . . . 17  |-  F/ t ( ( h `  Z )  =  0  /\  A. t  e.  T  ( 0  <_ 
( h `  t
)  /\  ( h `  t )  <_  1
) )
195 nfcv 2432 . . . . . . . . . . . . . . . . 17  |-  F/_ t A
196194, 195nfrab 2734 . . . . . . . . . . . . . . . 16  |-  F/_ t { h  e.  A  |  ( ( h `
 Z )  =  0  /\  A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 ) ) }
197111, 196nfcxfr 2429 . . . . . . . . . . . . . . 15  |-  F/_ t Q
198191, 197nfrab 2734 . . . . . . . . . . . . . 14  |-  F/_ t { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
199188, 198nfmpt 4124 . . . . . . . . . . . . 13  |-  F/_ t
( w  e.  X  |->  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
2002, 199nfcxfr 2429 . . . . . . . . . . . 12  |-  F/_ t G
201200nfrn 4937 . . . . . . . . . . 11  |-  F/_ t ran  G
202187, 201nffn 5356 . . . . . . . . . 10  |-  F/ t  g  Fn  ran  G
203 nfv 1609 . . . . . . . . . . 11  |-  F/ t ( g `  l
)  e.  l
204201, 203nfral 2609 . . . . . . . . . 10  |-  F/ t A. l  e.  ran  G ( g `  l
)  e.  l
205 nfcv 2432 . . . . . . . . . . 11  |-  F/_ t
f
206 nfcv 2432 . . . . . . . . . . 11  |-  F/_ t
( 1 ... m
)
207205, 206, 201nff1o 5486 . . . . . . . . . 10  |-  F/ t  f : ( 1 ... m ) -1-1-onto-> ran  G
208202, 204, 207nf3an 1786 . . . . . . . . 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 1783 . . . . . . . 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 1783 . . . . . . 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 1609 . . . . . . . . 9  |-  F/ w  m  e.  NN
212 nfcv 2432 . . . . . . . . . . 11  |-  F/_ w
g
213212, 22nffn 5356 . . . . . . . . . 10  |-  F/ w  g  Fn  ran  G
214 nfv 1609 . . . . . . . . . . 11  |-  F/ w
( g `  l
)  e.  l
21522, 214nfral 2609 . . . . . . . . . 10  |-  F/ w A. l  e.  ran  G ( g `  l
)  e.  l
216 nfcv 2432 . . . . . . . . . . 11  |-  F/_ w
f
217 nfcv 2432 . . . . . . . . . . 11  |-  F/_ w
( 1 ... m
)
218216, 217, 22nff1o 5486 . . . . . . . . . 10  |-  F/ w  f : ( 1 ... m ) -1-1-onto-> ran  G
219213, 215, 218nf3an 1786 . . . . . . . . 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 1783 . . . . . . . 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 1783 . . . . . . 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 27879 . . . . . 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 1614 . . . 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 1612 . . 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 1625 . . 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 1566 . 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 1530   E.wex 1531   F/wnf 1534    = wceq 1632    e. wcel 1696    =/= wne 2459   A.wral 2556   E.wrex 2557   {crab 2560   _Vcvv 2801    \ cdif 3162    C_ wss 3165   (/)c0 3468   U.cuni 3843   class class class wbr 4039    e. cmpt 4093   dom cdm 4705   ran crn 4706    Fn wfn 5266   -->wf 5267   -1-1-onto->wf1o 5270   ` cfv 5271  (class class class)co 5874   Fincfn 6879   0cc0 8753   1c1 8754    < clt 8883    <_ cle 8884   NNcn 9762   ...cfz 10798   #chash 11353
This theorem is referenced by:  stoweidlem53  27905
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-cnex 8809  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-mulcom 8817  ax-addass 8818  ax-mulass 8819  ax-distr 8820  ax-i2m1 8821  ax-1ne0 8822  ax-1rid 8823  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826  ax-pre-lttri 8827  ax-pre-lttrn 8828  ax-pre-ltadd 8829  ax-pre-mulgt0 8830
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 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-int 3879  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-1st 6138  df-2nd 6139  df-riota 6320  df-recs 6404  df-rdg 6439  df-1o 6495  df-oadd 6499  df-er 6676  df-en 6880  df-dom 6881  df-sdom 6882  df-fin 6883  df-card 7588  df-pnf 8885  df-mnf 8886  df-xr 8887  df-ltxr 8888  df-le 8889  df-sub 9055  df-neg 9056  df-nn 9763  df-n0 9982  df-z 10041  df-uz 10247  df-fz 10799  df-hash 11354
  Copyright terms: Public domain W3C validator