Theorem ramtcl

Description: The Ramsey number has the Ramsey number property if any number does. (Contributed by Mario Carneiro, 20-Apr-2015) (Revised by AV, 14-Sep-2020)

	Ref	Expression
Hypotheses	ramval.c	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
	ramval.t	⊢ 𝑇 = { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) }
Assertion	ramtcl	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( ( 𝑀 Ramsey 𝐹 ) ∈ 𝑇 ↔ 𝑇 ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		ramval.c	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
2		ramval.t	⊢ 𝑇 = { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) }
3		ne0i	⊢ ( ( 𝑀 Ramsey 𝐹 ) ∈ 𝑇 → 𝑇 ≠ ∅ )
4	1 2	ramcl2lem	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 𝑀 Ramsey 𝐹 ) = if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) )
5		ifnefalse	⊢ ( 𝑇 ≠ ∅ → if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) = inf ( 𝑇 , ℝ , < ) )
6	4 5	sylan9eq	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → ( 𝑀 Ramsey 𝐹 ) = inf ( 𝑇 , ℝ , < ) )
7	2	ssrab3	⊢ 𝑇 ⊆ ℕ0
8		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
9	7 8	sseqtri	⊢ 𝑇 ⊆ ( ℤ≥ ‘ 0 )
10	9	a1i	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → 𝑇 ⊆ ( ℤ≥ ‘ 0 ) )
11		infssuzcl	⊢ ( ( 𝑇 ⊆ ( ℤ≥ ‘ 0 ) ∧ 𝑇 ≠ ∅ ) → inf ( 𝑇 , ℝ , < ) ∈ 𝑇 )
12	10 11	sylan	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → inf ( 𝑇 , ℝ , < ) ∈ 𝑇 )
13	6 12	eqeltrd	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → ( 𝑀 Ramsey 𝐹 ) ∈ 𝑇 )
14	13	ex	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 𝑇 ≠ ∅ → ( 𝑀 Ramsey 𝐹 ) ∈ 𝑇 ) )
15	3 14	impbid2	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( ( 𝑀 Ramsey 𝐹 ) ∈ 𝑇 ↔ 𝑇 ≠ ∅ ) )