Metamath Proof Explorer

Theorem ramcl2

Description: The Ramsey number is either a nonnegative integer or plus infinity. (Contributed by Mario Carneiro, 20-Apr-2015) (Revised by AV, 14-Sep-2020)

Ref Expression
Assertion ramcl2 
|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) e. ( NN0 u. { +oo } ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )
2 eqid 
 |-  { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) ) } = { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) ) }
3 1 2 ramcl2lem 
 |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) = if ( { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) ) } = (/) , +oo , inf ( { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) ) } , RR , < ) ) )
4 iftrue 
 |-  ( { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) ) } = (/) -> if ( { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) ) } = (/) , +oo , inf ( { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) ) } , RR , < ) ) = +oo )
5 3 4 sylan9eq 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) ) } = (/) ) -> ( M Ramsey F ) = +oo )
6 ssun2 
 |-  { +oo } C_ ( NN0 u. { +oo } )
7 pnfex 
 |-  +oo e. _V
8 7 snss 
 |-  ( +oo e. ( NN0 u. { +oo } ) <-> { +oo } C_ ( NN0 u. { +oo } ) )
9 6 8 mpbir 
 |-  +oo e. ( NN0 u. { +oo } )
10 5 9 eqeltrdi 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) ) } = (/) ) -> ( M Ramsey F ) e. ( NN0 u. { +oo } ) )
11 ssun1 
 |-  NN0 C_ ( NN0 u. { +oo } )
12 1 2 ramtcl2 
 |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( ( M Ramsey F ) e. NN0 <-> { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) ) } =/= (/) ) )
13 12 biimpar 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) ) } =/= (/) ) -> ( M Ramsey F ) e. NN0 )
14 11 13 sseldi 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) ) } =/= (/) ) -> ( M Ramsey F ) e. ( NN0 u. { +oo } ) )
15 10 14 pm2.61dane 
 |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) e. ( NN0 u. { +oo } ) )