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	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
	ramval.t	⊢ 𝑇 = { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) }
Assertion	ramtub	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝑀 Ramsey 𝐹 ) ≤ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ramval.c	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
2		ramval.t	⊢ 𝑇 = { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) }
3	1 2	ramcl2lem	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 𝑀 Ramsey 𝐹 ) = if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) )
4		n0i	⊢ ( 𝐴 ∈ 𝑇 → ¬ 𝑇 = ∅ )
5	4	iffalsed	⊢ ( 𝐴 ∈ 𝑇 → if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) = inf ( 𝑇 , ℝ , < ) )
6	3 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		infssuzle	⊢ ( ( 𝑇 ⊆ ( ℤ≥ ‘ 0 ) ∧ 𝐴 ∈ 𝑇 ) → inf ( 𝑇 , ℝ , < ) ≤ 𝐴 )
12	10 11	sylan	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝐴 ∈ 𝑇 ) → inf ( 𝑇 , ℝ , < ) ≤ 𝐴 )
13	6 12	eqbrtrd	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝑀 Ramsey 𝐹 ) ≤ 𝐴 )