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

Theorem stoweidlem27 27444
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 5900 . . . 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 5615 . . . . 5  |-  ( F : ( 1 ... M ) -1-1-onto-> ran  G  ->  F  Fn  ( 1 ... M
) )
75, 6syl 16 . . . 4  |-  ( ph  ->  F  Fn  ( 1 ... M ) )
8 ovex 6045 . . . 4  |-  ( 1 ... M )  e. 
_V
9 fnex 5900 . . . 4  |-  ( ( F  Fn  ( 1 ... M )  /\  ( 1 ... M
)  e.  _V )  ->  F  e.  _V )
107, 8, 9sylancl 644 . . 3  |-  ( ph  ->  F  e.  _V )
11 coexg 5352 . . 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 5614 . . . . . . 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 5549 . . . . . 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 5076 . . . . . 6  |-  ran  ( Y  o.  F )  C_ 
ran  Y
19 fvelrnb 5713 . . . . . . . . . . . 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 5057 . . . . . . . . . . . . . . . 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 4239 . . . . . . . . . . . . . . . . . . 19  |-  F/_ w
( w  e.  X  |->  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }
)
2923, 28nfcxfr 2520 . . . . . . . . . . . . . . . . . 18  |-  F/_ w G
3029nfrn 5052 . . . . . . . . . . . . . . . . 17  |-  F/_ w ran  G
3130nfcri 2517 . . . . . . . . . . . . . . . 16  |-  F/ w  l  e.  ran  G
3227, 31nfan 1836 . . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . . . . . . . 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 2523 . . . . . . . . . . . . . . . . . . 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 5667 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h  =  ( Y `  l )  ->  (
h `  t )  =  ( ( Y `
 l ) `  t ) )
4241breq2d 4165 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  ( Y `  l )  ->  (
0  <  ( h `  t )  <->  0  <  ( ( Y `  l
) `  t )
) )
4342rabbidv 2891 . . . . . . . . . . . . . . . . . . . 20  |-  ( h  =  ( Y `  l )  ->  { t  e.  T  |  0  <  ( h `  t ) }  =  { t  e.  T  |  0  <  (
( Y `  l
) `  t ) } )
4443eqeq2d 2398 . . . . . . . . . . . . . . . . . . 19  |-  ( h  =  ( Y `  l )  ->  (
w  =  { t  e.  T  |  0  <  ( h `  t ) }  <->  w  =  { t  e.  T  |  0  <  (
( Y `  l
) `  t ) } ) )
4538, 39, 40, 44elrabf 3034 . . . . . . . . . . . . . . . . . 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 2770 . . . . . . . . . . . . . 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 2447 . . . . . . . . . . . 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 2761 . . . . . . . . . 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 2772 . . . . . . . . 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 3297 . . . . . 6  |-  ( ph  ->  ran  Y  C_  Q
)
6218, 61syl5ss 3302 . . . . 5  |-  ( ph  ->  ran  ( Y  o.  F )  C_  Q
)
63 df-f 5398 . . . . 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 3291 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( T  \  U ) )  ->  t  e.  U. X )
68 eluni 3960 . . . . . . . . 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 1836 . . . . . . . . 9  |-  F/ w
( ph  /\  t  e.  ( T  \  U
) )
7223funmpt2 5430 . . . . . . . . . . . . . . 15  |-  Fun  G
7323dmeqi 5011 . . . . . . . . . . . . . . . . . 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 27363 . . . . . . . . . . . . . . . . . . . . . . 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 2730 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A. w  e.  X  { h  e.  Q  |  w  =  {
t  e.  T  | 
0  <  ( h `  t ) } }  e.  _V )
80 dmmptg 5307 . . . . . . . . . . . . . . . . . . 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 2431 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  G  =  X )
8382eleq2d 2454 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( w  e.  dom  G  <-> 
w  e.  X ) )
8483biimpar 472 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  w  e.  X )  ->  w  e.  dom  G )
85 fvelrn 5805 . . . . . . . . . . . . . . 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 5621 . . . . . . . . . . . . . . . . . . . 20  |-  ( F : ( 1 ... M ) -1-1-onto-> ran  G  ->  F : ( 1 ... M ) -onto-> ran  G
)
89 forn 5596 . . . . . . . . . . . . . . . . . . . 20  |-  ( F : ( 1 ... M ) -onto-> ran  G  ->  ran  F  =  ran  G )
905, 88, 893syl 19 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ran  F  =  ran  G )
9190eleq2d 2454 . . . . . . . . . . . . . . . . . 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 5713 . . . . . . . . . . . . . . . . . 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 2655 . . . . . . . . . . . . . . . 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 5739 . . . . . . . . . . . . . . . . . . . . 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 5668 . . . . . . . . . . . . . . . . . . . . 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 2419 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  ( G `  w )  e.  ran  G )  /\  ( i  e.  ( 1 ... M )  /\  ( F `  i )  =  ( G `  w ) ) )  ->  (
( Y  o.  F
) `  i )  =  ( Y `  ( G `  w ) ) )
106 eleq1 2447 . . . . . . . . . . . . . . . . . . . . . . . 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 2448 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( l  =  ( G `  w )  ->  (
( Y `  l
)  e.  l  <->  ( Y `  l )  e.  ( G `  w ) ) )
109 fveq2 5668 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( l  =  ( G `  w )  ->  ( Y `  l )  =  ( Y `  ( G `  w ) ) )
110109eleq1d 2453 . . . . . . . . . . . . . . . . . . . . . . . 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 2954 . . . . . . . . . . . . . . . . . . . . 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 2461 . . . . . . . . . . . . . . . . . 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 2655 . . . . . . . . . . . . . 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 5751 . . . . . . . . . . . . . . . . . . . . . . 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 2454 . . . . . . . . . . . . . . . . . . . . 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 2523 . . . . . . . . . . . . . . . . . . . 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 5667 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( h  =  ( ( Y  o.  F ) `  i )  ->  (
h `  t )  =  ( ( ( Y  o.  F ) `
 i ) `  t ) )
134133breq2d 4165 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h  =  ( ( Y  o.  F ) `  i )  ->  (
0  <  ( h `  t )  <->  0  <  ( ( ( Y  o.  F ) `  i
) `  t )
) )
135134rabbidv 2891 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  ( ( Y  o.  F ) `  i )  ->  { t  e.  T  |  0  <  ( h `  t ) }  =  { t  e.  T  |  0  <  (
( ( Y  o.  F ) `  i
) `  t ) } )
136135eqeq2d 2398 . . . . . . . . . . . . . . . . . . . 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 3034 . . . . . . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . . . . . 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 2827 . . . . . . . . . . . . . . . 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 2760 . . . . . . . . . . . 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 1778 . . . . . . . 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 1814 . . . . . . 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 2730 . . . 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 5516 . . . . 5  |-  ( q  =  ( Y  o.  F )  ->  (
q : ( 1 ... M ) --> Q  <-> 
( Y  o.  F
) : ( 1 ... M ) --> Q ) )
160 fveq1 5667 . . . . . . . . 9  |-  ( q  =  ( Y  o.  F )  ->  (
q `  i )  =  ( ( Y  o.  F ) `  i ) )
161160fveq1d 5670 . . . . . . . 8  |-  ( q  =  ( Y  o.  F )  ->  (
( q `  i
) `  t )  =  ( ( ( Y  o.  F ) `
 i ) `  t ) )
162161breq2d 4165 . . . . . . 7  |-  ( q  =  ( Y  o.  F )  ->  (
0  <  ( (
q `  i ) `  t )  <->  0  <  ( ( ( Y  o.  F ) `  i
) `  t )
) )
163162rexbidv 2670 . . . . . 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 2669 . . . . 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 2980 . 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 1717   F/_wnfc 2510   A.wral 2649   E.wrex 2650   {crab 2653   _Vcvv 2899    \ cdif 3260    C_ wss 3263   U.cuni 3957   class class class wbr 4153    e. cmpt 4207   dom cdm 4818   ran crn 4819    o. ccom 4822   Fun wfun 5388    Fn wfn 5389   -->wf 5390   -onto->wfo 5392   -1-1-onto->wf1o 5393   ` cfv 5394  (class class class)co 6020   0cc0 8923   1c1 8924    < clt 9053   NNcn 9932   ...cfz 10975
This theorem is referenced by:  stoweidlem35  27452
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 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-rep 4261  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641
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 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-reu 2656  df-rab 2658  df-v 2901  df-sbc 3105  df-csb 3195  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-iun 4037  df-br 4154  df-opab 4208  df-mpt 4209  df-id 4439  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831  df-iota 5358  df-fun 5396  df-fn 5397  df-f 5398  df-f1 5399  df-fo 5400  df-f1o 5401  df-fv 5402  df-ov 6023
  Copyright terms: Public domain W3C validator