Theorem ramtub

Description: The Ramsey number is a lower bound on the set of all numbers 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	ramtub	|- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ A e. T ) -> ( M Ramsey F ) <_ A )

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		n0i	|- ( A e. T -> -. T = (/) )
5	4	iffalsed	|- ( A e. T -> if ( T = (/) , +oo , inf ( T , RR , < ) ) = inf ( T , RR , < ) )
6	3 5	sylan9eq	|- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ A e. T ) -> ( M Ramsey F ) = inf ( T , RR , < ) )
7	2	ssrab3	|- T C_ NN0
8		nn0uz	|- NN0 = ( ZZ>= ` 0 )
9	7 8	sseqtri	|- T C_ ( ZZ>= ` 0 )
10	9	a1i	|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> T C_ ( ZZ>= ` 0 ) )
11		infssuzle	|- ( ( T C_ ( ZZ>= ` 0 ) /\ A e. T ) -> inf ( T , RR , < ) <_ A )
12	10 11	sylan	|- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ A e. T ) -> inf ( T , RR , < ) <_ A )
13	6 12	eqbrtrd	|- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ A e. T ) -> ( M Ramsey F ) <_ A )