Metamath Proof Explorer

Theorem ramval

Description: The value of the Ramsey number function. (Contributed by Mario Carneiro, 21-Apr-2015) (Revised by AV, 14-Sep-2020)

Ref Expression
Hypotheses ramval.c 
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )
ramval.t 
|- T = { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) }
Assertion ramval 
|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) = inf ( T , RR* , < ) )

Proof

Step Hyp Ref Expression
1 ramval.c 
 |-  C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )
2 ramval.t 
 |-  T = { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) }
3 df-ram 
 |-  Ramsey = ( m e. NN0 , r e. _V |-> inf ( { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) ) } , RR* , < ) )
4 3 a1i 
 |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> Ramsey = ( m e. NN0 , r e. _V |-> inf ( { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) ) } , RR* , < ) ) )
5 simplrr 
 |-  ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) -> r = F )
6 5 dmeqd 
 |-  ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) -> dom r = dom F )
7 simpll3 
 |-  ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) -> F : R --> NN0 )
8 7 fdmd 
 |-  ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) -> dom F = R )
9 6 8 eqtrd 
 |-  ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) -> dom r = R )
10 simplrl 
 |-  ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) -> m = M )
11 10 eqeq2d 
 |-  ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) -> ( ( # ` y ) = m <-> ( # ` y ) = M ) )
12 11 rabbidv 
 |-  ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) -> { y e. ~P s | ( # ` y ) = m } = { y e. ~P s | ( # ` y ) = M } )
13 vex 
 |-  s e. _V
14 simpll1 
 |-  ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) -> M e. NN0 )
15 1 hashbcval 
 |-  ( ( s e. _V /\ M e. NN0 ) -> ( s C M ) = { y e. ~P s | ( # ` y ) = M } )
16 13 14 15 sylancr 
 |-  ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) -> ( s C M ) = { y e. ~P s | ( # ` y ) = M } )
17 12 16 eqtr4d 
 |-  ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) -> { y e. ~P s | ( # ` y ) = m } = ( s C M ) )
18 9 17 oveq12d 
 |-  ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) -> ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) = ( R ^m ( s C M ) ) )
19 18 raleqdv 
 |-  ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) -> ( A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) <-> A. f e. ( R ^m ( s C M ) ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) ) )
20 simpr 
 |-  ( ( m = M /\ r = F ) -> r = F )
21 20 dmeqd 
 |-  ( ( m = M /\ r = F ) -> dom r = dom F )
22 fdm 
 |-  ( F : R --> NN0 -> dom F = R )
23 22 3ad2ant3 
 |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> dom F = R )
24 21 23 sylan9eqr 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) -> dom r = R )
25 24 ad2antrr 
 |-  ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) -> dom r = R )
26 5 ad2antrr 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> r = F )
27 26 fveq1d 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> ( r ` c ) = ( F ` c ) )
28 27 breq1d 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> ( ( r ` c ) <_ ( # ` x ) <-> ( F ` c ) <_ ( # ` x ) ) )
29 10 ad2antrr 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> m = M )
30 29 oveq2d 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> ( x C m ) = ( x C M ) )
31 vex 
 |-  x e. _V
32 14 ad2antrr 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> M e. NN0 )
33 29 32 eqeltrd 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> m e. NN0 )
34 1 hashbcval 
 |-  ( ( x e. _V /\ m e. NN0 ) -> ( x C m ) = { y e. ~P x | ( # ` y ) = m } )
35 31 33 34 sylancr 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> ( x C m ) = { y e. ~P x | ( # ` y ) = m } )
36 30 35 eqtr3d 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> ( x C M ) = { y e. ~P x | ( # ` y ) = m } )
37 36 sseq1d 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> ( ( x C M ) C_ ( `' f " { c } ) <-> { y e. ~P x | ( # ` y ) = m } C_ ( `' f " { c } ) ) )
38 rabss 
 |-  ( { y e. ~P x | ( # ` y ) = m } C_ ( `' f " { c } ) <-> A. y e. ~P x ( ( # ` y ) = m -> y e. ( `' f " { c } ) ) )
39 36 eleq2d 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> ( y e. ( x C M ) <-> y e. { y e. ~P x | ( # ` y ) = m } ) )
40 rabid 
 |-  ( y e. { y e. ~P x | ( # ` y ) = m } <-> ( y e. ~P x /\ ( # ` y ) = m ) )
41 39 40 bitrdi 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> ( y e. ( x C M ) <-> ( y e. ~P x /\ ( # ` y ) = m ) ) )
42 41 biimpar 
 |-  ( ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) /\ ( y e. ~P x /\ ( # ` y ) = m ) ) -> y e. ( x C M ) )
43 elpwi 
 |-  ( x e. ~P s -> x C_ s )
44 43 adantl 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> x C_ s )
45 1 hashbcss 
 |-  ( ( s e. _V /\ x C_ s /\ M e. NN0 ) -> ( x C M ) C_ ( s C M ) )
46 13 44 32 45 mp3an2i 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> ( x C M ) C_ ( s C M ) )
47 46 sselda 
 |-  ( ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) /\ y e. ( x C M ) ) -> y e. ( s C M ) )
48 42 47 syldan 
 |-  ( ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) /\ ( y e. ~P x /\ ( # ` y ) = m ) ) -> y e. ( s C M ) )
49 elmapi 
 |-  ( f e. ( R ^m ( s C M ) ) -> f : ( s C M ) --> R )
50 49 ad3antlr 
 |-  ( ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) /\ ( y e. ~P x /\ ( # ` y ) = m ) ) -> f : ( s C M ) --> R )
51 ffn 
 |-  ( f : ( s C M ) --> R -> f Fn ( s C M ) )
52 fniniseg 
 |-  ( f Fn ( s C M ) -> ( y e. ( `' f " { c } ) <-> ( y e. ( s C M ) /\ ( f ` y ) = c ) ) )
53 50 51 52 3syl 
 |-  ( ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) /\ ( y e. ~P x /\ ( # ` y ) = m ) ) -> ( y e. ( `' f " { c } ) <-> ( y e. ( s C M ) /\ ( f ` y ) = c ) ) )
54 48 53 mpbirand 
 |-  ( ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) /\ ( y e. ~P x /\ ( # ` y ) = m ) ) -> ( y e. ( `' f " { c } ) <-> ( f ` y ) = c ) )
55 54 anassrs 
 |-  ( ( ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) /\ y e. ~P x ) /\ ( # ` y ) = m ) -> ( y e. ( `' f " { c } ) <-> ( f ` y ) = c ) )
56 55 pm5.74da 
 |-  ( ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) /\ y e. ~P x ) -> ( ( ( # ` y ) = m -> y e. ( `' f " { c } ) ) <-> ( ( # ` y ) = m -> ( f ` y ) = c ) ) )
57 56 ralbidva 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> ( A. y e. ~P x ( ( # ` y ) = m -> y e. ( `' f " { c } ) ) <-> A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) )
58 38 57 syl5bb 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> ( { y e. ~P x | ( # ` y ) = m } C_ ( `' f " { c } ) <-> A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) )
59 37 58 bitr2d 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> ( A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) <-> ( x C M ) C_ ( `' f " { c } ) ) )
60 28 59 anbi12d 
 |-  ( ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) /\ x e. ~P s ) -> ( ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) <-> ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) )
61 60 rexbidva 
 |-  ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) -> ( E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) <-> E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) )
62 25 61 rexeqbidv 
 |-  ( ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) /\ f e. ( R ^m ( s C M ) ) ) -> ( E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) <-> E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) )
63 62 ralbidva 
 |-  ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) -> ( A. f e. ( R ^m ( s C M ) ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) <-> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) )
64 19 63 bitrd 
 |-  ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) -> ( A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) <-> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) )
65 64 imbi2d 
 |-  ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) -> ( ( n <_ ( # ` s ) -> A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) ) <-> ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) ) )
66 65 albidv 
 |-  ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) /\ n e. NN0 ) -> ( A. s ( n <_ ( # ` s ) -> A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) ) <-> A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) ) )
67 66 rabbidva 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) -> { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) ) } = { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) } )
68 67 2 eqtr4di 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) -> { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) ) } = T )
69 68 infeq1d 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( m = M /\ r = F ) ) -> inf ( { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) ) } , RR* , < ) = inf ( T , RR* , < ) )
70 simp1 
 |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> M e. NN0 )
71 simp3 
 |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> F : R --> NN0 )
72 simp2 
 |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> R e. V )
73 71 72 fexd 
 |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> F e. _V )
74 xrltso 
 |-  < Or RR*
75 74 infex 
 |-  inf ( T , RR* , < ) e. _V
76 75 a1i 
 |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> inf ( T , RR* , < ) e. _V )
77 4 69 70 73 76 ovmpod 
 |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) = inf ( T , RR* , < ) )