Metamath Proof Explorer

Theorem ramcl2lem

Description: Lemma for extended real closure of the Ramsey number function. (Contributed by Mario Carneiro, 20-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 ramcl2lem 
|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) = if ( T = (/) , +oo , 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 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 , < ) ) )