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 |
|
fex |
|- ( ( F : R --> NN0 /\ R e. V ) -> F e. _V ) |
74 |
71 72 73
|
syl2anc |
|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> F e. _V ) |
75 |
|
xrltso |
|- < Or RR* |
76 |
75
|
infex |
|- inf ( T , RR* , < ) e. _V |
77 |
76
|
a1i |
|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> inf ( T , RR* , < ) e. _V ) |
78 |
4 69 70 74 77
|
ovmpod |
|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) = inf ( T , RR* , < ) ) |