Metamath Proof Explorer

Theorem ramtcl2

Description: The Ramsey number is an integer iff there is a number with the Ramsey number property. (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 ramtcl2
|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( ( M Ramsey F ) e. NN0 <-> T =/= (/) ) )

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 1 2 ramcl2lem
|-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) = if ( T = (/) , +oo , inf ( T , RR , < ) ) )
4 3 eleq1d
|-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( ( M Ramsey F ) e. NN0 <-> if ( T = (/) , +oo , inf ( T , RR , < ) ) e. NN0 ) )
5 pnfnre
|-  +oo e/ RR
6 5 neli
|-  -. +oo e. RR
7 iftrue
|-  ( T = (/) -> if ( T = (/) , +oo , inf ( T , RR , < ) ) = +oo )
8 7 eleq1d
|-  ( T = (/) -> ( if ( T = (/) , +oo , inf ( T , RR , < ) ) e. NN0 <-> +oo e. NN0 ) )
9 nn0re
|-  ( +oo e. NN0 -> +oo e. RR )
10 8 9 syl6bi
|-  ( T = (/) -> ( if ( T = (/) , +oo , inf ( T , RR , < ) ) e. NN0 -> +oo e. RR ) )
11 6 10 mtoi
|-  ( T = (/) -> -. if ( T = (/) , +oo , inf ( T , RR , < ) ) e. NN0 )
12 11 necon2ai
|-  ( if ( T = (/) , +oo , inf ( T , RR , < ) ) e. NN0 -> T =/= (/) )
13 4 12 syl6bi
|-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( ( M Ramsey F ) e. NN0 -> T =/= (/) ) )
14 1 2 ramtcl
|-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( ( M Ramsey F ) e. T <-> T =/= (/) ) )
15 2 ssrab3
|-  T C_ NN0
16 15 sseli
|-  ( ( M Ramsey F ) e. T -> ( M Ramsey F ) e. NN0 )
17 14 16 syl6bir
|-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( T =/= (/) -> ( M Ramsey F ) e. NN0 ) )
18 13 17 impbid
|-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( ( M Ramsey F ) e. NN0 <-> T =/= (/) ) )