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	⊢ 𝑇 = { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) }
Assertion	ramtlecl	⊢ ( 𝑀 ∈ 𝑇 → ( ℤ≥ ‘ 𝑀 ) ⊆ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		ramtlecl.t	⊢ 𝑇 = { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) }
2		breq1	⊢ ( 𝑛 = 𝑀 → ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) ↔ 𝑀 ≤ ( ♯ ‘ 𝑠 ) ) )
3	2	imbi1d	⊢ ( 𝑛 = 𝑀 → ( ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) ↔ ( 𝑀 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) ) )
4	3	albidv	⊢ ( 𝑛 = 𝑀 → ( ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) ↔ ∀ 𝑠 ( 𝑀 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) ) )
5	4 1	elrab2	⊢ ( 𝑀 ∈ 𝑇 ↔ ( 𝑀 ∈ ℕ0 ∧ ∀ 𝑠 ( 𝑀 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) ) )
6	5	simplbi	⊢ ( 𝑀 ∈ 𝑇 → 𝑀 ∈ ℕ0 )
7		eluznn0	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑛 ∈ ℕ0 )
8	7	ex	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑛 ∈ ℕ0 ) )
9	8	ssrdv	⊢ ( 𝑀 ∈ ℕ0 → ( ℤ≥ ‘ 𝑀 ) ⊆ ℕ0 )
10	6 9	syl	⊢ ( 𝑀 ∈ 𝑇 → ( ℤ≥ ‘ 𝑀 ) ⊆ ℕ0 )
11	5	simprbi	⊢ ( 𝑀 ∈ 𝑇 → ∀ 𝑠 ( 𝑀 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) )
12		eluzle	⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑛 )
13	12	adantl	⊢ ( ( 𝑀 ∈ 𝑇 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ≤ 𝑛 )
14		nn0ssre	⊢ ℕ0 ⊆ ℝ
15		ressxr	⊢ ℝ ⊆ ℝ*
16	14 15	sstri	⊢ ℕ0 ⊆ ℝ*
17	6	adantr	⊢ ( ( 𝑀 ∈ 𝑇 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ∈ ℕ0 )
18	16 17	sseldi	⊢ ( ( 𝑀 ∈ 𝑇 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ∈ ℝ* )
19	6 7	sylan	⊢ ( ( 𝑀 ∈ 𝑇 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑛 ∈ ℕ0 )
20	16 19	sseldi	⊢ ( ( 𝑀 ∈ 𝑇 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑛 ∈ ℝ* )
21		vex	⊢ 𝑠 ∈ V
22		hashxrcl	⊢ ( 𝑠 ∈ V → ( ♯ ‘ 𝑠 ) ∈ ℝ* )
23	21 22	mp1i	⊢ ( ( 𝑀 ∈ 𝑇 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ♯ ‘ 𝑠 ) ∈ ℝ* )
24		xrletr	⊢ ( ( 𝑀 ∈ ℝ* ∧ 𝑛 ∈ ℝ* ∧ ( ♯ ‘ 𝑠 ) ∈ ℝ* ) → ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ ( ♯ ‘ 𝑠 ) ) → 𝑀 ≤ ( ♯ ‘ 𝑠 ) ) )
25	18 20 23 24	syl3anc	⊢ ( ( 𝑀 ∈ 𝑇 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ ( ♯ ‘ 𝑠 ) ) → 𝑀 ≤ ( ♯ ‘ 𝑠 ) ) )
26	13 25	mpand	⊢ ( ( 𝑀 ∈ 𝑇 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → 𝑀 ≤ ( ♯ ‘ 𝑠 ) ) )
27	26	imim1d	⊢ ( ( 𝑀 ∈ 𝑇 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑀 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) → ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) ) )
28	27	ralrimdva	⊢ ( 𝑀 ∈ 𝑇 → ( ( 𝑀 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) ) )
29	28	alimdv	⊢ ( 𝑀 ∈ 𝑇 → ( ∀ 𝑠 ( 𝑀 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) → ∀ 𝑠 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) ) )
30	11 29	mpd	⊢ ( 𝑀 ∈ 𝑇 → ∀ 𝑠 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) )
31		ralcom4	⊢ ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) ↔ ∀ 𝑠 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) )
32	30 31	sylibr	⊢ ( 𝑀 ∈ 𝑇 → ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) )
33		ssrab	⊢ ( ( ℤ≥ ‘ 𝑀 ) ⊆ { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) } ↔ ( ( ℤ≥ ‘ 𝑀 ) ⊆ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) ) )
34	10 32 33	sylanbrc	⊢ ( 𝑀 ∈ 𝑇 → ( ℤ≥ ‘ 𝑀 ) ⊆ { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → 𝜑 ) } )
35	34 1	sseqtrrdi	⊢ ( 𝑀 ∈ 𝑇 → ( ℤ≥ ‘ 𝑀 ) ⊆ 𝑇 )