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 =/= (/) ) )

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 =/= (/) ) )

Metamath Proof Explorer

Theorem ramtcl2

Proof