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

Theorem stoweidlem27 27643
Description: This lemma is used to prove the existence of a function p as in Lemma 1 [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
stoweidlem27.1  |-  G  =  ( w  e.  X  |->  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
stoweidlem27.2  |-  ( ph  ->  Q  e.  _V )
stoweidlem27.3  |-  ( ph  ->  M  e.  NN )
stoweidlem27.4  |-  ( ph  ->  Y  Fn  ran  G
)
stoweidlem27.5  |-  ( ph  ->  ran  G  e.  _V )
stoweidlem27.6  |-  ( (
ph  /\  l  e.  ran  G )  ->  ( Y `  l )  e.  l )
stoweidlem27.7  |-  ( ph  ->  F : ( 1 ... M ) -1-1-onto-> ran  G
)
stoweidlem27.8  |-  ( ph  ->  ( T  \  U
)  C_  U. X )
stoweidlem27.9  |-  F/ t
ph
stoweidlem27.10  |-  F/ w ph
stoweidlem27.11  |-  F/_ h Q
Assertion
Ref Expression
stoweidlem27  |-  ( ph  ->  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, F    h, l, Y, t, w    T, h, w    i, q, t, F    i, G    i, M, q    i, X, w   
i, Y, q    ph, i    Q, l    ph, l    G, l    Q, q    T, q    U, q    w, M    w, Q    w, U
Allowed substitution hints:    ph( w, t, h, q)    Q( t, h, i)    T( t, i, l)    U( t, h, i, l)    F( l)    G( w, t, h, q)    M( t, h, l)    X( t, h, q, l)

Proof of Theorem stoweidlem27
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 stoweidlem27.4 . . . 4  |-  ( ph  ->  Y  Fn  ran  G
)
2 stoweidlem27.5 . . . 4  |-  ( ph  ->  ran  G  e.  _V )
3 fnex 5920 . . . 4  |-  ( ( Y  Fn  ran  G  /\  ran  G  e.  _V )  ->  Y  e.  _V )
41, 2, 3syl2anc 643 . . 3  |-  ( ph  ->  Y  e.  _V )
5 stoweidlem27.7 . . . . 5  |-  ( ph  ->  F : ( 1 ... M ) -1-1-onto-> ran  G
)
6 f1ofn 5634 . . . . 5  |-  ( F : ( 1 ... M ) -1-1-onto-> ran  G  ->  F  Fn  ( 1 ... M
) )
75, 6syl 16 . . . 4  |-  ( ph  ->  F  Fn  ( 1 ... M ) )
8 ovex 6065 . . . 4  |-  ( 1 ... M )  e. 
_V
9 fnex 5920 . . . 4  |-  ( ( F  Fn  ( 1 ... M )  /\  ( 1 ... M
)  e.  _V )  ->  F  e.  _V )
107, 8, 9sylancl 644 . . 3  |-  ( ph  ->  F  e.  _V )
11 coexg 5371 . . 3  |-  ( ( Y  e.  _V  /\  F  e.  _V )  ->  ( Y  o.  F
)  e.  _V )
124, 10, 11syl2anc 643 . 2  |-  ( ph  ->  ( Y  o.  F
)  e.  _V )
13 stoweidlem27.3 . . 3  |-  ( ph  ->  M  e.  NN )
14 f1of 5633 . . . . . . 7  |-  ( F : ( 1 ... M ) -1-1-onto-> ran  G  ->  F : ( 1 ... M ) --> ran  G
)
155, 14syl 16 . . . . . 6  |-  ( ph  ->  F : ( 1 ... M ) --> ran 
G )
16 fnfco 5568 . . . . . 6  |-  ( ( Y  Fn  ran  G  /\  F : ( 1 ... M ) --> ran 
G )  ->  ( Y  o.  F )  Fn  ( 1 ... M
) )
171, 15, 16syl2anc 643 . . . . 5  |-  ( ph  ->  ( Y  o.  F
)  Fn  ( 1 ... M ) )
18 rncoss 5095 . . . . . 6  |-  ran  ( Y  o.  F )  C_ 
ran  Y
19 fvelrnb 5733 . . . . . . . . . . . 12  |-  ( Y  Fn  ran  G  -> 
( k  e.  ran  Y  <->  E. l  e.  ran  G ( Y `  l
)  =  k ) )
201, 19syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( k  e.  ran  Y  <->  E. l  e.  ran  G ( Y `  l
)  =  k ) )
2120biimpa 471 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ran  Y )  ->  E. l  e.  ran  G ( Y `
 l )  =  k )
22 simpr 448 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  l  e.  ran  G )  ->  l  e.  ran  G )
23 stoweidlem27.1 . . . . . . . . . . . . . . . . 17  |-  G  =  ( w  e.  X  |->  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
2423elrnmpt 5076 . . . . . . . . . . . . . . . 16  |-  ( l  e.  ran  G  -> 
( l  e.  ran  G  <->  E. w  e.  X  l  =  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } } ) )
2522, 24syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  l  e.  ran  G )  ->  (
l  e.  ran  G  <->  E. w  e.  X  l  =  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } } ) )
2622, 25mpbid 202 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  l  e.  ran  G )  ->  E. w  e.  X  l  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
27 stoweidlem27.10 . . . . . . . . . . . . . . . 16  |-  F/ w ph
28 nfmpt1 4258 . . . . . . . . . . . . . . . . . . 19  |-  F/_ w
( w  e.  X  |->  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
2923, 28nfcxfr 2537 . . . . . . . . . . . . . . . . . 18  |-  F/_ w G
3029nfrn 5071 . . . . . . . . . . . . . . . . 17  |-  F/_ w ran  G
3130nfcri 2534 . . . . . . . . . . . . . . . 16  |-  F/ w  l  e.  ran  G
3227, 31nfan 1842 . . . . . . . . . . . . . . 15  |-  F/ w
( ph  /\  l  e.  ran  G )
33 nfv 1626 . . . . . . . . . . . . . . 15  |-  F/ w
( Y `  l
)  e.  Q
34 stoweidlem27.6 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  l  e.  ran  G )  ->  ( Y `  l )  e.  l )
3534ad2antrr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  l  e.  ran  G )  /\  w  e.  X
)  /\  l  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)  ->  ( Y `  l )  e.  l )
36 simpr 448 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  l  e.  ran  G )  /\  w  e.  X
)  /\  l  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)  ->  l  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
3735, 36eleqtrd 2480 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  l  e.  ran  G )  /\  w  e.  X
)  /\  l  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)  ->  ( Y `  l )  e.  {
h  e.  Q  |  w  =  { t  e.  T  |  0  <  ( h `  t
) } } )
38 nfcv 2540 . . . . . . . . . . . . . . . . . . 19  |-  F/_ h
( Y `  l
)
39 stoweidlem27.11 . . . . . . . . . . . . . . . . . . 19  |-  F/_ h Q
40 nfv 1626 . . . . . . . . . . . . . . . . . . 19  |-  F/ h  w  =  { t  e.  T  |  0  <  ( ( Y `  l ) `  t
) }
41 fveq1 5686 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h  =  ( Y `  l )  ->  (
h `  t )  =  ( ( Y `
 l ) `  t ) )
4241breq2d 4184 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  ( Y `  l )  ->  (
0  <  ( h `  t )  <->  0  <  ( ( Y `  l
) `  t )
) )
4342rabbidv 2908 . . . . . . . . . . . . . . . . . . . 20  |-  ( h  =  ( Y `  l )  ->  { t  e.  T  |  0  <  ( h `  t ) }  =  { t  e.  T  |  0  <  (
( Y `  l
) `  t ) } )
4443eqeq2d 2415 . . . . . . . . . . . . . . . . . . 19  |-  ( h  =  ( Y `  l )  ->  (
w  =  { t  e.  T  |  0  <  ( h `  t ) }  <->  w  =  { t  e.  T  |  0  <  (
( Y `  l
) `  t ) } ) )
4538, 39, 40, 44elrabf 3051 . . . . . . . . . . . . . . . . . 18  |-  ( ( Y `  l )  e.  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } }  <->  ( ( Y `
 l )  e.  Q  /\  w  =  { t  e.  T  |  0  <  (
( Y `  l
) `  t ) } ) )
4637, 45sylib 189 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  l  e.  ran  G )  /\  w  e.  X
)  /\  l  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)  ->  ( ( Y `  l )  e.  Q  /\  w  =  { t  e.  T  |  0  <  (
( Y `  l
) `  t ) } ) )
4746simpld 446 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  l  e.  ran  G )  /\  w  e.  X
)  /\  l  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)  ->  ( Y `  l )  e.  Q
)
4847exp31 588 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  l  e.  ran  G )  ->  (
w  e.  X  -> 
( l  =  {
h  e.  Q  |  w  =  { t  e.  T  |  0  <  ( h `  t
) } }  ->  ( Y `  l )  e.  Q ) ) )
4932, 33, 48rexlimd 2787 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  l  e.  ran  G )  ->  ( E. w  e.  X  l  =  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } }  ->  ( Y `
 l )  e.  Q ) )
5026, 49mpd 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  l  e.  ran  G )  ->  ( Y `  l )  e.  Q )
5150adantlr 696 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ran  Y )  /\  l  e.  ran  G )  ->  ( Y `  l )  e.  Q
)
52 eleq1 2464 . . . . . . . . . . . 12  |-  ( ( Y `  l )  =  k  ->  (
( Y `  l
)  e.  Q  <->  k  e.  Q ) )
5351, 52syl5ibcom 212 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ran  Y )  /\  l  e.  ran  G )  ->  ( ( Y `
 l )  =  k  ->  k  e.  Q ) )
5453reximdva 2778 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ran  Y )  ->  ( E. l  e.  ran  G ( Y `  l
)  =  k  ->  E. l  e.  ran  G  k  e.  Q ) )
5521, 54mpd 15 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ran  Y )  ->  E. l  e.  ran  G  k  e.  Q )
56 idd 22 . . . . . . . . . . 11  |-  ( l  e.  ran  G  -> 
( k  e.  Q  ->  k  e.  Q ) )
5756a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ran  Y )  ->  (
l  e.  ran  G  ->  ( k  e.  Q  ->  k  e.  Q ) ) )
5857rexlimdv 2789 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ran  Y )  ->  ( E. l  e.  ran  G  k  e.  Q  -> 
k  e.  Q ) )
5955, 58mpd 15 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ran  Y )  ->  k  e.  Q )
6059ex 424 . . . . . . 7  |-  ( ph  ->  ( k  e.  ran  Y  ->  k  e.  Q
) )
6160ssrdv 3314 . . . . . 6  |-  ( ph  ->  ran  Y  C_  Q
)
6218, 61syl5ss 3319 . . . . 5  |-  ( ph  ->  ran  ( Y  o.  F )  C_  Q
)
63 df-f 5417 . . . . 5  |-  ( ( Y  o.  F ) : ( 1 ... M ) --> Q  <->  ( ( Y  o.  F )  Fn  ( 1 ... M
)  /\  ran  ( Y  o.  F )  C_  Q ) )
6417, 62, 63sylanbrc 646 . . . 4  |-  ( ph  ->  ( Y  o.  F
) : ( 1 ... M ) --> Q )
65 stoweidlem27.9 . . . . 5  |-  F/ t
ph
66 stoweidlem27.8 . . . . . . . . . 10  |-  ( ph  ->  ( T  \  U
)  C_  U. X )
6766sselda 3308 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( T  \  U ) )  ->  t  e.  U. X )
68 eluni 3978 . . . . . . . . 9  |-  ( t  e.  U. X  <->  E. w
( t  e.  w  /\  w  e.  X
) )
6967, 68sylib 189 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( T  \  U ) )  ->  E. w
( t  e.  w  /\  w  e.  X
) )
70 nfv 1626 . . . . . . . . . 10  |-  F/ w  t  e.  ( T  \  U )
7127, 70nfan 1842 . . . . . . . . 9  |-  F/ w
( ph  /\  t  e.  ( T  \  U
) )
7223funmpt2 5449 . . . . . . . . . . . . . . 15  |-  Fun  G
7323dmeqi 5030 . . . . . . . . . . . . . . . . . 18  |-  dom  G  =  dom  ( w  e.  X  |->  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } } )
74 stoweidlem27.2 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  Q  e.  _V )
7539rabexgf 27562 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Q  e.  _V  ->  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } }  e.  _V )
7674, 75syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }  e.  _V )
7776adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  w  e.  X )  ->  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } }  e.  _V )
7877ex 424 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( w  e.  X  ->  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }  e.  _V ) )
7927, 78ralrimi 2747 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A. w  e.  X  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }  e.  _V )
80 dmmptg 5326 . . . . . . . . . . . . . . . . . . 19  |-  ( A. w  e.  X  {
h  e.  Q  |  w  =  { t  e.  T  |  0  <  ( h `  t
) } }  e.  _V  ->  dom  ( w  e.  X  |->  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } } )  =  X )
8179, 80syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  dom  ( w  e.  X  |->  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  (
h `  t ) } } )  =  X )
8273, 81syl5eq 2448 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  G  =  X )
8382eleq2d 2471 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( w  e.  dom  G  <-> 
w  e.  X ) )
8483biimpar 472 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  w  e.  X )  ->  w  e.  dom  G )
85 fvelrn 5825 . . . . . . . . . . . . . . 15  |-  ( ( Fun  G  /\  w  e.  dom  G )  -> 
( G `  w
)  e.  ran  G
)
8672, 84, 85sylancr 645 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  w  e.  X )  ->  ( G `  w )  e.  ran  G )
8786adantrl 697 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( t  e.  w  /\  w  e.  X ) )  -> 
( G `  w
)  e.  ran  G
)
88 f1ofo 5640 . . . . . . . . . . . . . . . . . . . 20  |-  ( F : ( 1 ... M ) -1-1-onto-> ran  G  ->  F : ( 1 ... M ) -onto-> ran  G
)
89 forn 5615 . . . . . . . . . . . . . . . . . . . 20  |-  ( F : ( 1 ... M ) -onto-> ran  G  ->  ran  F  =  ran  G )
905, 88, 893syl 19 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ran  F  =  ran  G )
9190eleq2d 2471 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( G `  w )  e.  ran  F  <-> 
( G `  w
)  e.  ran  G
) )
9291biimpar 472 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( G `  w )  e.  ran  G )  ->  ( G `  w )  e.  ran  F )
937adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( G `  w )  e.  ran  G )  ->  F  Fn  ( 1 ... M
) )
94 fvelrnb 5733 . . . . . . . . . . . . . . . . . 18  |-  ( F  Fn  ( 1 ... M )  ->  (
( G `  w
)  e.  ran  F  <->  E. i  e.  ( 1 ... M ) ( F `  i )  =  ( G `  w ) ) )
9593, 94syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( G `  w )  e.  ran  G )  ->  ( ( G `  w )  e.  ran  F  <->  E. i  e.  ( 1 ... M
) ( F `  i )  =  ( G `  w ) ) )
9692, 95mpbid 202 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( G `  w )  e.  ran  G )  ->  E. i  e.  ( 1 ... M
) ( F `  i )  =  ( G `  w ) )
97 df-rex 2672 . . . . . . . . . . . . . . . 16  |-  ( E. i  e.  ( 1 ... M ) ( F `  i )  =  ( G `  w )  <->  E. i
( i  e.  ( 1 ... M )  /\  ( F `  i )  =  ( G `  w ) ) )
9896, 97sylib 189 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( G `  w )  e.  ran  G )  ->  E. i
( i  e.  ( 1 ... M )  /\  ( F `  i )  =  ( G `  w ) ) )
99 simprl 733 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ( G `  w )  e.  ran  G )  /\  ( i  e.  ( 1 ... M )  /\  ( F `  i )  =  ( G `  w ) ) )  ->  i  e.  ( 1 ... M
) )
10015ad2antrr 707 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  ( G `  w )  e.  ran  G )  /\  ( i  e.  ( 1 ... M )  /\  ( F `  i )  =  ( G `  w ) ) )  ->  F : ( 1 ... M ) --> ran  G
)
101 fvco3 5759 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F : ( 1 ... M ) --> ran 
G  /\  i  e.  ( 1 ... M
) )  ->  (
( Y  o.  F
) `  i )  =  ( Y `  ( F `  i ) ) )
102100, 99, 101syl2anc 643 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  ( G `  w )  e.  ran  G )  /\  ( i  e.  ( 1 ... M )  /\  ( F `  i )  =  ( G `  w ) ) )  ->  (
( Y  o.  F
) `  i )  =  ( Y `  ( F `  i ) ) )
103 fveq2 5687 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F `  i )  =  ( G `  w )  ->  ( Y `  ( F `  i ) )  =  ( Y `  ( G `  w )
) )
104103ad2antll 710 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  ( G `  w )  e.  ran  G )  /\  ( i  e.  ( 1 ... M )  /\  ( F `  i )  =  ( G `  w ) ) )  ->  ( Y `  ( F `  i ) )  =  ( Y `  ( G `  w )
) )
105102, 104eqtrd 2436 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  ( G `  w )  e.  ran  G )  /\  ( i  e.  ( 1 ... M )  /\  ( F `  i )  =  ( G `  w ) ) )  ->  (
( Y  o.  F
) `  i )  =  ( Y `  ( G `  w ) ) )
106 eleq1 2464 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( l  =  ( G `  w )  ->  (
l  e.  ran  G  <->  ( G `  w )  e.  ran  G ) )
107106anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( l  =  ( G `  w )  ->  (
( ph  /\  l  e.  ran  G )  <->  ( ph  /\  ( G `  w
)  e.  ran  G
) ) )
108 eleq2 2465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( l  =  ( G `  w )  ->  (
( Y `  l
)  e.  l  <->  ( Y `  l )  e.  ( G `  w ) ) )
109 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( l  =  ( G `  w )  ->  ( Y `  l )  =  ( Y `  ( G `  w ) ) )
110109eleq1d 2470 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( l  =  ( G `  w )  ->  (
( Y `  l
)  e.  ( G `
 w )  <->  ( Y `  ( G `  w
) )  e.  ( G `  w ) ) )
111108, 110bitrd 245 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( l  =  ( G `  w )  ->  (
( Y `  l
)  e.  l  <->  ( Y `  ( G `  w
) )  e.  ( G `  w ) ) )
112107, 111imbi12d 312 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( l  =  ( G `  w )  ->  (
( ( ph  /\  l  e.  ran  G )  ->  ( Y `  l )  e.  l )  <->  ( ( ph  /\  ( G `  w
)  e.  ran  G
)  ->  ( Y `  ( G `  w
) )  e.  ( G `  w ) ) ) )
113112, 34vtoclg 2971 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( G `  w )  e.  ran  G  -> 
( ( ph  /\  ( G `  w )  e.  ran  G )  ->  ( Y `  ( G `  w ) )  e.  ( G `
 w ) ) )
114113anabsi7 793 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( G `  w )  e.  ran  G )  ->  ( Y `  ( G `  w
) )  e.  ( G `  w ) )
115114adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  ( G `  w )  e.  ran  G )  /\  ( i  e.  ( 1 ... M )  /\  ( F `  i )  =  ( G `  w ) ) )  ->  ( Y `  ( G `  w ) )  e.  ( G `  w
) )
116105, 115eqeltrd 2478 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ( G `  w )  e.  ran  G )  /\  ( i  e.  ( 1 ... M )  /\  ( F `  i )  =  ( G `  w ) ) )  ->  (
( Y  o.  F
) `  i )  e.  ( G `  w
) )
11799, 116jca 519 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  ( G `  w )  e.  ran  G )  /\  ( i  e.  ( 1 ... M )  /\  ( F `  i )  =  ( G `  w ) ) )  ->  (
i  e.  ( 1 ... M )  /\  ( ( Y  o.  F ) `  i
)  e.  ( G `
 w ) ) )
118117ex 424 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( G `  w )  e.  ran  G )  ->  ( (
i  e.  ( 1 ... M )  /\  ( F `  i )  =  ( G `  w ) )  -> 
( i  e.  ( 1 ... M )  /\  ( ( Y  o.  F ) `  i )  e.  ( G `  w ) ) ) )
119118eximdv 1629 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( G `  w )  e.  ran  G )  ->  ( E. i ( i  e.  ( 1 ... M
)  /\  ( F `  i )  =  ( G `  w ) )  ->  E. i
( i  e.  ( 1 ... M )  /\  ( ( Y  o.  F ) `  i )  e.  ( G `  w ) ) ) )
12098, 119mpd 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( G `  w )  e.  ran  G )  ->  E. i
( i  e.  ( 1 ... M )  /\  ( ( Y  o.  F ) `  i )  e.  ( G `  w ) ) )
121 df-rex 2672 . . . . . . . . . . . . . 14  |-  ( E. i  e.  ( 1 ... M ) ( ( Y  o.  F
) `  i )  e.  ( G `  w
)  <->  E. i ( i  e.  ( 1 ... M )  /\  (
( Y  o.  F
) `  i )  e.  ( G `  w
) ) )
122120, 121sylibr 204 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( G `  w )  e.  ran  G )  ->  E. i  e.  ( 1 ... M
) ( ( Y  o.  F ) `  i )  e.  ( G `  w ) )
12387, 122syldan 457 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( t  e.  w  /\  w  e.  X ) )  ->  E. i  e.  (
1 ... M ) ( ( Y  o.  F
) `  i )  e.  ( G `  w
) )
124 simplrl 737 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
t  e.  w  /\  w  e.  X )
)  /\  ( ( Y  o.  F ) `  i )  e.  ( G `  w ) )  ->  t  e.  w )
125 simpr 448 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  w  e.  X )  ->  w  e.  X )
12623fvmpt2 5771 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( w  e.  X  /\  { h  e.  Q  |  w  =  { t  e.  T  |  0  <  ( h `  t
) } }  e.  _V )  ->  ( G `
 w )  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
127125, 77, 126syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  w  e.  X )  ->  ( G `  w )  =  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
128127eleq2d 2471 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  w  e.  X )  ->  (
( ( Y  o.  F ) `  i
)  e.  ( G `
 w )  <->  ( ( Y  o.  F ) `  i )  e.  {
h  e.  Q  |  w  =  { t  e.  T  |  0  <  ( h `  t
) } } ) )
129128biimpa 471 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  w  e.  X )  /\  (
( Y  o.  F
) `  i )  e.  ( G `  w
) )  ->  (
( Y  o.  F
) `  i )  e.  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
130129adantlrl 701 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
t  e.  w  /\  w  e.  X )
)  /\  ( ( Y  o.  F ) `  i )  e.  ( G `  w ) )  ->  ( ( Y  o.  F ) `  i )  e.  {
h  e.  Q  |  w  =  { t  e.  T  |  0  <  ( h `  t
) } } )
131 nfcv 2540 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ h
( ( Y  o.  F ) `  i
)
132 nfv 1626 . . . . . . . . . . . . . . . . . . . 20  |-  F/ h  w  =  { t  e.  T  |  0  <  ( ( ( Y  o.  F ) `  i ) `  t
) }
133 fveq1 5686 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( h  =  ( ( Y  o.  F ) `  i )  ->  (
h `  t )  =  ( ( ( Y  o.  F ) `
 i ) `  t ) )
134133breq2d 4184 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h  =  ( ( Y  o.  F ) `  i )  ->  (
0  <  ( h `  t )  <->  0  <  ( ( ( Y  o.  F ) `  i
) `  t )
) )
135134rabbidv 2908 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  ( ( Y  o.  F ) `  i )  ->  { t  e.  T  |  0  <  ( h `  t ) }  =  { t  e.  T  |  0  <  (
( ( Y  o.  F ) `  i
) `  t ) } )
136135eqeq2d 2415 . . . . . . . . . . . . . . . . . . . 20  |-  ( h  =  ( ( Y  o.  F ) `  i )  ->  (
w  =  { t  e.  T  |  0  <  ( h `  t ) }  <->  w  =  { t  e.  T  |  0  <  (
( ( Y  o.  F ) `  i
) `  t ) } ) )
137131, 39, 132, 136elrabf 3051 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( Y  o.  F
) `  i )  e.  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }  <->  ( ( ( Y  o.  F ) `  i
)  e.  Q  /\  w  =  { t  e.  T  |  0  <  ( ( ( Y  o.  F ) `  i ) `  t
) } ) )
138130, 137sylib 189 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
t  e.  w  /\  w  e.  X )
)  /\  ( ( Y  o.  F ) `  i )  e.  ( G `  w ) )  ->  ( (
( Y  o.  F
) `  i )  e.  Q  /\  w  =  { t  e.  T  |  0  <  (
( ( Y  o.  F ) `  i
) `  t ) } ) )
139138simprd 450 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
t  e.  w  /\  w  e.  X )
)  /\  ( ( Y  o.  F ) `  i )  e.  ( G `  w ) )  ->  w  =  { t  e.  T  |  0  <  (
( ( Y  o.  F ) `  i
) `  t ) } )
140124, 139eleqtrd 2480 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
t  e.  w  /\  w  e.  X )
)  /\  ( ( Y  o.  F ) `  i )  e.  ( G `  w ) )  ->  t  e.  { t  e.  T  | 
0  <  ( (
( Y  o.  F
) `  i ) `  t ) } )
141 rabid 2844 . . . . . . . . . . . . . . . 16  |-  ( t  e.  { t  e.  T  |  0  < 
( ( ( Y  o.  F ) `  i ) `  t
) }  <->  ( t  e.  T  /\  0  <  ( ( ( Y  o.  F ) `  i ) `  t
) ) )
142140, 141sylib 189 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
t  e.  w  /\  w  e.  X )
)  /\  ( ( Y  o.  F ) `  i )  e.  ( G `  w ) )  ->  ( t  e.  T  /\  0  <  ( ( ( Y  o.  F ) `  i ) `  t
) ) )
143142simprd 450 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
t  e.  w  /\  w  e.  X )
)  /\  ( ( Y  o.  F ) `  i )  e.  ( G `  w ) )  ->  0  <  ( ( ( Y  o.  F ) `  i
) `  t )
)
144143ex 424 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( t  e.  w  /\  w  e.  X ) )  -> 
( ( ( Y  o.  F ) `  i )  e.  ( G `  w )  ->  0  <  (
( ( Y  o.  F ) `  i
) `  t )
) )
145144reximdv 2777 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( t  e.  w  /\  w  e.  X ) )  -> 
( E. i  e.  ( 1 ... M
) ( ( Y  o.  F ) `  i )  e.  ( G `  w )  ->  E. i  e.  ( 1 ... M ) 0  <  ( ( ( Y  o.  F
) `  i ) `  t ) ) )
146123, 145mpd 15 . . . . . . . . . . 11  |-  ( (
ph  /\  ( t  e.  w  /\  w  e.  X ) )  ->  E. i  e.  (
1 ... M ) 0  <  ( ( ( Y  o.  F ) `
 i ) `  t ) )
147146ex 424 . . . . . . . . . 10  |-  ( ph  ->  ( ( t  e.  w  /\  w  e.  X )  ->  E. i  e.  ( 1 ... M
) 0  <  (
( ( Y  o.  F ) `  i
) `  t )
) )
148147adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( T  \  U ) )  ->  ( (
t  e.  w  /\  w  e.  X )  ->  E. i  e.  ( 1 ... M ) 0  <  ( ( ( Y  o.  F
) `  i ) `  t ) ) )
14971, 148eximd 1782 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( T  \  U ) )  ->  ( E. w ( t  e.  w  /\  w  e.  X )  ->  E. w E. i  e.  (
1 ... M ) 0  <  ( ( ( Y  o.  F ) `
 i ) `  t ) ) )
15069, 149mpd 15 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( T  \  U ) )  ->  E. w E. i  e.  (
1 ... M ) 0  <  ( ( ( Y  o.  F ) `
 i ) `  t ) )
151 nfv 1626 . . . . . . . 8  |-  F/ w E. i  e.  (
1 ... M ) 0  <  ( ( ( Y  o.  F ) `
 i ) `  t )
152 idd 22 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( T  \  U ) )  ->  ( E. i  e.  ( 1 ... M ) 0  <  ( ( ( Y  o.  F ) `
 i ) `  t )  ->  E. i  e.  ( 1 ... M
) 0  <  (
( ( Y  o.  F ) `  i
) `  t )
) )
15371, 151, 152exlimd 1820 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( T  \  U ) )  ->  ( E. w E. i  e.  ( 1 ... M ) 0  <  ( ( ( Y  o.  F
) `  i ) `  t )  ->  E. i  e.  ( 1 ... M
) 0  <  (
( ( Y  o.  F ) `  i
) `  t )
) )
154150, 153mpd 15 . . . . . 6  |-  ( (
ph  /\  t  e.  ( T  \  U ) )  ->  E. i  e.  ( 1 ... M
) 0  <  (
( ( Y  o.  F ) `  i
) `  t )
)
155154ex 424 . . . . 5  |-  ( ph  ->  ( t  e.  ( T  \  U )  ->  E. i  e.  ( 1 ... M ) 0  <  ( ( ( Y  o.  F
) `  i ) `  t ) ) )
15665, 155ralrimi 2747 . . . 4  |-  ( ph  ->  A. t  e.  ( T  \  U ) E. i  e.  ( 1 ... M ) 0  <  ( ( ( Y  o.  F
) `  i ) `  t ) )
15764, 156jca 519 . . 3  |-  ( ph  ->  ( ( Y  o.  F ) : ( 1 ... M ) --> Q  /\  A. t  e.  ( T  \  U
) E. i  e.  ( 1 ... M
) 0  <  (
( ( Y  o.  F ) `  i
) `  t )
) )
15813, 157jca 519 . 2  |-  ( ph  ->  ( M  e.  NN  /\  ( ( Y  o.  F ) : ( 1 ... M ) --> Q  /\  A. t  e.  ( T  \  U
) E. i  e.  ( 1 ... M
) 0  <  (
( ( Y  o.  F ) `  i
) `  t )
) ) )
159 feq1 5535 . . . . 5  |-  ( q  =  ( Y  o.  F )  ->  (
q : ( 1 ... M ) --> Q  <-> 
( Y  o.  F
) : ( 1 ... M ) --> Q ) )
160 fveq1 5686 . . . . . . . . 9  |-  ( q  =  ( Y  o.  F )  ->  (
q `  i )  =  ( ( Y  o.  F ) `  i ) )
161160fveq1d 5689 . . . . . . . 8  |-  ( q  =  ( Y  o.  F )  ->  (
( q `  i
) `  t )  =  ( ( ( Y  o.  F ) `
 i ) `  t ) )
162161breq2d 4184 . . . . . . 7  |-  ( q  =  ( Y  o.  F )  ->  (
0  <  ( (
q `  i ) `  t )  <->  0  <  ( ( ( Y  o.  F ) `  i
) `  t )
) )
163162rexbidv 2687 . . . . . 6  |-  ( q  =  ( Y  o.  F )  ->  ( E. i  e.  (
1 ... M ) 0  <  ( ( q `
 i ) `  t )  <->  E. i  e.  ( 1 ... M
) 0  <  (
( ( Y  o.  F ) `  i
) `  t )
) )
164163ralbidv 2686 . . . . 5  |-  ( q  =  ( Y  o.  F )  ->  ( A. t  e.  ( T  \  U ) E. i  e.  ( 1 ... M ) 0  <  ( ( q `
 i ) `  t )  <->  A. t  e.  ( T  \  U
) E. i  e.  ( 1 ... M
) 0  <  (
( ( Y  o.  F ) `  i
) `  t )
) )
165159, 164anbi12d 692 . . . 4  |-  ( q  =  ( Y  o.  F )  ->  (
( q : ( 1 ... M ) --> Q  /\  A. t  e.  ( T  \  U
) E. i  e.  ( 1 ... M
) 0  <  (
( q `  i
) `  t )
)  <->  ( ( Y  o.  F ) : ( 1 ... M
) --> Q  /\  A. t  e.  ( T  \  U ) E. i  e.  ( 1 ... M
) 0  <  (
( ( Y  o.  F ) `  i
) `  t )
) ) )
166165anbi2d 685 . . 3  |-  ( q  =  ( Y  o.  F )  ->  (
( M  e.  NN  /\  ( q : ( 1 ... M ) --> Q  /\  A. t  e.  ( T  \  U
) E. i  e.  ( 1 ... M
) 0  <  (
( q `  i
) `  t )
) )  <->  ( M  e.  NN  /\  ( ( Y  o.  F ) : ( 1 ... M ) --> Q  /\  A. t  e.  ( T 
\  U ) E. i  e.  ( 1 ... M ) 0  <  ( ( ( Y  o.  F ) `
 i ) `  t ) ) ) ) )
167166spcegv 2997 . 2  |-  ( ( Y  o.  F )  e.  _V  ->  (
( M  e.  NN  /\  ( ( Y  o.  F ) : ( 1 ... M ) --> Q  /\  A. t  e.  ( T  \  U
) E. i  e.  ( 1 ... M
) 0  <  (
( ( Y  o.  F ) `  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 )
) ) ) )
16812, 158, 167sylc 58 1  |-  ( ph  ->  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:    -> wi 4    <-> wb 177    /\ wa 359   E.wex 1547   F/wnf 1550    = wceq 1649    e. wcel 1721   F/_wnfc 2527   A.wral 2666   E.wrex 2667   {crab 2670   _Vcvv 2916    \ cdif 3277    C_ wss 3280   U.cuni 3975   class class class wbr 4172    e. cmpt 4226   dom cdm 4837   ran crn 4838    o. ccom 4841   Fun wfun 5407    Fn wfn 5408   -->wf 5409   -onto->wfo 5411   -1-1-onto->wf1o 5412   ` cfv 5413  (class class class)co 6040   0cc0 8946   1c1 8947    < clt 9076   NNcn 9956   ...cfz 10999
This theorem is referenced by:  stoweidlem35  27651
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043
  Copyright terms: Public domain W3C validator