Theorem ramtlecl

Description: The set T of numbers with the Ramsey number property is upward-closed. (Contributed by Mario Carneiro, 21-Apr-2015)

	Ref	Expression
Hypothesis	ramtlecl.t	$$⊢T=\left\{n\in {\mathbb{N}}_0|\forall s\left(n\le \left|s\right|\to \phi \right)\right\}$$
Assertion	ramtlecl	$$⊢M\in T\to {\mathbb{Z}}_{\ge M}\subseteq T$$

Proof

Step	Hyp	Ref	Expression
1		ramtlecl.t	$$⊢T=\left\{n\in {\mathbb{N}}_0|\forall s\left(n\le \left|s\right|\to \phi \right)\right\}$$
2		breq1	$$⊢n=M\to \left(n\le \left|s\right|\leftrightarrow M\le \left|s\right|\right)$$
3	2	imbi1d	$$⊢n=M\to \left(\left(n\le \left|s\right|\to \phi \right)\leftrightarrow \left(M\le \left|s\right|\to \phi \right)\right)$$
4	3	albidv	$$⊢n=M\to \left(\forall s\left(n\le \left|s\right|\to \phi \right)\leftrightarrow \forall s\left(M\le \left|s\right|\to \phi \right)\right)$$
5	4 1	elrab2	$$⊢M\in T\leftrightarrow \left(M\in {\mathbb{N}}_0\wedge \forall s\left(M\le \left|s\right|\to \phi \right)\right)$$
6	5	simplbi	$$⊢M\in T\to M\in {\mathbb{N}}_0$$
7		eluznn0	$$⊢\left(M\in {\mathbb{N}}_0\wedge n\in {\mathbb{Z}}_{\ge M}\right)\to n\in {\mathbb{N}}_0$$
8	7	ex	$$⊢M\in {\mathbb{N}}_0\to \left(n\in {\mathbb{Z}}_{\ge M}\to n\in {\mathbb{N}}_0\right)$$
9	8	ssrdv	$$⊢M\in {\mathbb{N}}_0\to {\mathbb{Z}}_{\ge M}\subseteq {\mathbb{N}}_0$$
10	6 9	syl	$$⊢M\in T\to {\mathbb{Z}}_{\ge M}\subseteq {\mathbb{N}}_0$$
11	5	simprbi	$$⊢M\in T\to \forall s\left(M\le \left|s\right|\to \phi \right)$$
12		eluzle	$$⊢n\in {\mathbb{Z}}_{\ge M}\to M\le n$$
13	12	adantl	$$⊢\left(M\in T\wedge n\in {\mathbb{Z}}_{\ge M}\right)\to M\le n$$
14		nn0ssre	$$⊢{\mathbb{N}}_0\subseteq ℝ$$
15		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
16	14 15	sstri	$$⊢{\mathbb{N}}_0\subseteq {ℝ}^{*}$$
17	6	adantr	$$⊢\left(M\in T\wedge n\in {\mathbb{Z}}_{\ge M}\right)\to M\in {\mathbb{N}}_0$$
18	16 17	sselid	$$⊢\left(M\in T\wedge n\in {\mathbb{Z}}_{\ge M}\right)\to M\in {ℝ}^{*}$$
19	6 7	sylan	$$⊢\left(M\in T\wedge n\in {\mathbb{Z}}_{\ge M}\right)\to n\in {\mathbb{N}}_0$$
20	16 19	sselid	$$⊢\left(M\in T\wedge n\in {\mathbb{Z}}_{\ge M}\right)\to n\in {ℝ}^{*}$$
21		vex	$$⊢s\in \mathrm{V}$$
22		hashxrcl	$$⊢s\in \mathrm{V}\to \left|s\right|\in {ℝ}^{*}$$
23	21 22	mp1i	$$⊢\left(M\in T\wedge n\in {\mathbb{Z}}_{\ge M}\right)\to \left|s\right|\in {ℝ}^{*}$$
24		xrletr	$$⊢\left(M\in {ℝ}^{*}\wedge n\in {ℝ}^{*}\wedge \left|s\right|\in {ℝ}^{*}\right)\to \left(\left(M\le n\wedge n\le \left|s\right|\right)\to M\le \left|s\right|\right)$$
25	18 20 23 24	syl3anc	$$⊢\left(M\in T\wedge n\in {\mathbb{Z}}_{\ge M}\right)\to \left(\left(M\le n\wedge n\le \left|s\right|\right)\to M\le \left|s\right|\right)$$
26	13 25	mpand	$$⊢\left(M\in T\wedge n\in {\mathbb{Z}}_{\ge M}\right)\to \left(n\le \left|s\right|\to M\le \left|s\right|\right)$$
27	26	imim1d	$$⊢\left(M\in T\wedge n\in {\mathbb{Z}}_{\ge M}\right)\to \left(\left(M\le \left|s\right|\to \phi \right)\to \left(n\le \left|s\right|\to \phi \right)\right)$$
28	27	ralrimdva	$$⊢M\in T\to \left(\left(M\le \left|s\right|\to \phi \right)\to \forall n\in {\mathbb{Z}}_{\ge M}\left(n\le \left|s\right|\to \phi \right)\right)$$
29	28	alimdv	$$⊢M\in T\to \left(\forall s\left(M\le \left|s\right|\to \phi \right)\to \forall s\forall n\in {\mathbb{Z}}_{\ge M}\left(n\le \left|s\right|\to \phi \right)\right)$$
30	11 29	mpd	$$⊢M\in T\to \forall s\forall n\in {\mathbb{Z}}_{\ge M}\left(n\le \left|s\right|\to \phi \right)$$
31		ralcom4	$$⊢\forall n\in {\mathbb{Z}}_{\ge M}\forall s\left(n\le \left|s\right|\to \phi \right)\leftrightarrow \forall s\forall n\in {\mathbb{Z}}_{\ge M}\left(n\le \left|s\right|\to \phi \right)$$
32	30 31	sylibr	$$⊢M\in T\to \forall n\in {\mathbb{Z}}_{\ge M}\forall s\left(n\le \left|s\right|\to \phi \right)$$
33		ssrab	$$⊢{\mathbb{Z}}_{\ge M}\subseteq \left\{n\in {\mathbb{N}}_0|\forall s\left(n\le \left|s\right|\to \phi \right)\right\}\leftrightarrow \left({\mathbb{Z}}_{\ge M}\subseteq {\mathbb{N}}_0\wedge \forall n\in {\mathbb{Z}}_{\ge M}\forall s\left(n\le \left|s\right|\to \phi \right)\right)$$
34	10 32 33	sylanbrc	$$⊢M\in T\to {\mathbb{Z}}_{\ge M}\subseteq \left\{n\in {\mathbb{N}}_0|\forall s\left(n\le \left|s\right|\to \phi \right)\right\}$$
35	34 1	sseqtrrdi	$$⊢M\in T\to {\mathbb{Z}}_{\ge M}\subseteq T$$