Theorem ramxrcl

Description: The Ramsey number is an extended real number. (This theorem does not imply Ramsey's theorem, unlike ramcl .) (Contributed by Mario Carneiro, 20-Apr-2015)

	Ref	Expression
Assertion	ramxrcl	|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) e. RR* )

Proof

Step	Hyp	Ref	Expression
1		nn0ssre	|- NN0 C_ RR
2		ressxr	|- RR C_ RR*
3	1 2	sstri	|- NN0 C_ RR*
4		pnfxr	|- +oo e. RR*
5		snssi	|- ( +oo e. RR* -> { +oo } C_ RR* )
6	4 5	ax-mp	|- { +oo } C_ RR*
7	3 6	unssi	|- ( NN0 u. { +oo } ) C_ RR*
8		ramcl2	|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) e. ( NN0 u. { +oo } ) )
9	7 8	sseldi	|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) e. RR* )