Metamath Proof Explorer

Theorem ramubcl

Description: If the Ramsey number is upper bounded, then it is an integer. (Contributed by Mario Carneiro, 20-Apr-2015)

Ref Expression
Assertion ramubcl 
|- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( A e. NN0 /\ ( M Ramsey F ) <_ A ) ) -> ( M Ramsey F ) e. NN0 )

Proof

Step Hyp Ref Expression
1 nn0re 
 |-  ( A e. NN0 -> A e. RR )
2 ltpnf 
 |-  ( A e. RR -> A < +oo )
3 rexr 
 |-  ( A e. RR -> A e. RR* )
4 pnfxr 
 |-  +oo e. RR*
5 xrltnle 
 |-  ( ( A e. RR* /\ +oo e. RR* ) -> ( A < +oo <-> -. +oo <_ A ) )
6 3 4 5 sylancl 
 |-  ( A e. RR -> ( A < +oo <-> -. +oo <_ A ) )
7 2 6 mpbid 
 |-  ( A e. RR -> -. +oo <_ A )
8 1 7 syl 
 |-  ( A e. NN0 -> -. +oo <_ A )
9 8 ad2antrl 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( A e. NN0 /\ ( M Ramsey F ) <_ A ) ) -> -. +oo <_ A )
10 simprr 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( A e. NN0 /\ ( M Ramsey F ) <_ A ) ) -> ( M Ramsey F ) <_ A )
11 breq1 
 |-  ( ( M Ramsey F ) = +oo -> ( ( M Ramsey F ) <_ A <-> +oo <_ A ) )
12 10 11 syl5ibcom 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( A e. NN0 /\ ( M Ramsey F ) <_ A ) ) -> ( ( M Ramsey F ) = +oo -> +oo <_ A ) )
13 9 12 mtod 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( A e. NN0 /\ ( M Ramsey F ) <_ A ) ) -> -. ( M Ramsey F ) = +oo )
14 elsni 
 |-  ( ( M Ramsey F ) e. { +oo } -> ( M Ramsey F ) = +oo )
15 13 14 nsyl 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( A e. NN0 /\ ( M Ramsey F ) <_ A ) ) -> -. ( M Ramsey F ) e. { +oo } )
16 ramcl2 
 |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) e. ( NN0 u. { +oo } ) )
17 16 adantr 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( A e. NN0 /\ ( M Ramsey F ) <_ A ) ) -> ( M Ramsey F ) e. ( NN0 u. { +oo } ) )
18 elun 
 |-  ( ( M Ramsey F ) e. ( NN0 u. { +oo } ) <-> ( ( M Ramsey F ) e. NN0 \/ ( M Ramsey F ) e. { +oo } ) )
19 17 18 sylib 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( A e. NN0 /\ ( M Ramsey F ) <_ A ) ) -> ( ( M Ramsey F ) e. NN0 \/ ( M Ramsey F ) e. { +oo } ) )
20 19 ord 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( A e. NN0 /\ ( M Ramsey F ) <_ A ) ) -> ( -. ( M Ramsey F ) e. NN0 -> ( M Ramsey F ) e. { +oo } ) )
21 15 20 mt3d 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( A e. NN0 /\ ( M Ramsey F ) <_ A ) ) -> ( M Ramsey F ) e. NN0 )