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 |
|
eqeq2 |
|- ( +oo = if ( T = (/) , +oo , inf ( T , RR , < ) ) -> ( ( M Ramsey F ) = +oo <-> ( M Ramsey F ) = if ( T = (/) , +oo , inf ( T , RR , < ) ) ) ) |
4 |
|
eqeq2 |
|- ( inf ( T , RR , < ) = if ( T = (/) , +oo , inf ( T , RR , < ) ) -> ( ( M Ramsey F ) = inf ( T , RR , < ) <-> ( M Ramsey F ) = if ( T = (/) , +oo , inf ( T , RR , < ) ) ) ) |
5 |
1 2
|
ramval |
|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) = inf ( T , RR* , < ) ) |
6 |
|
infeq1 |
|- ( T = (/) -> inf ( T , RR* , < ) = inf ( (/) , RR* , < ) ) |
7 |
|
xrinf0 |
|- inf ( (/) , RR* , < ) = +oo |
8 |
6 7
|
eqtrdi |
|- ( T = (/) -> inf ( T , RR* , < ) = +oo ) |
9 |
5 8
|
sylan9eq |
|- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ T = (/) ) -> ( M Ramsey F ) = +oo ) |
10 |
|
df-ne |
|- ( T =/= (/) <-> -. T = (/) ) |
11 |
5
|
adantr |
|- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ T =/= (/) ) -> ( M Ramsey F ) = inf ( T , RR* , < ) ) |
12 |
|
xrltso |
|- < Or RR* |
13 |
12
|
a1i |
|- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ T =/= (/) ) -> < Or RR* ) |
14 |
2
|
ssrab3 |
|- T C_ NN0 |
15 |
|
nn0ssre |
|- NN0 C_ RR |
16 |
14 15
|
sstri |
|- T C_ RR |
17 |
|
nn0uz |
|- NN0 = ( ZZ>= ` 0 ) |
18 |
14 17
|
sseqtri |
|- T C_ ( ZZ>= ` 0 ) |
19 |
18
|
a1i |
|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> T C_ ( ZZ>= ` 0 ) ) |
20 |
|
infssuzcl |
|- ( ( T C_ ( ZZ>= ` 0 ) /\ T =/= (/) ) -> inf ( T , RR , < ) e. T ) |
21 |
19 20
|
sylan |
|- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ T =/= (/) ) -> inf ( T , RR , < ) e. T ) |
22 |
16 21
|
sseldi |
|- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ T =/= (/) ) -> inf ( T , RR , < ) e. RR ) |
23 |
22
|
rexrd |
|- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ T =/= (/) ) -> inf ( T , RR , < ) e. RR* ) |
24 |
22
|
adantr |
|- ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ T =/= (/) ) /\ z e. T ) -> inf ( T , RR , < ) e. RR ) |
25 |
16
|
a1i |
|- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ T =/= (/) ) -> T C_ RR ) |
26 |
25
|
sselda |
|- ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ T =/= (/) ) /\ z e. T ) -> z e. RR ) |
27 |
|
simpr |
|- ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ T =/= (/) ) /\ z e. T ) -> z e. T ) |
28 |
|
infssuzle |
|- ( ( T C_ ( ZZ>= ` 0 ) /\ z e. T ) -> inf ( T , RR , < ) <_ z ) |
29 |
18 27 28
|
sylancr |
|- ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ T =/= (/) ) /\ z e. T ) -> inf ( T , RR , < ) <_ z ) |
30 |
24 26 29
|
lensymd |
|- ( ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ T =/= (/) ) /\ z e. T ) -> -. z < inf ( T , RR , < ) ) |
31 |
13 23 21 30
|
infmin |
|- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ T =/= (/) ) -> inf ( T , RR* , < ) = inf ( T , RR , < ) ) |
32 |
11 31
|
eqtrd |
|- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ T =/= (/) ) -> ( M Ramsey F ) = inf ( T , RR , < ) ) |
33 |
10 32
|
sylan2br |
|- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ -. T = (/) ) -> ( M Ramsey F ) = inf ( T , RR , < ) ) |
34 |
3 4 9 33
|
ifbothda |
|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) = if ( T = (/) , +oo , inf ( T , RR , < ) ) ) |