Theorem ramtcl2

Description: The Ramsey number is an integer iff there is a number 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	ramtcl2	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 ↔ 𝑇 ≠ ∅ ) )

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	3	eleq1d	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 ↔ if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) ∈ ℕ0 ) )
5		pnfnre	⊢ +∞ ∉ ℝ
6	5	neli	⊢ ¬ +∞ ∈ ℝ
7		iftrue	⊢ ( 𝑇 = ∅ → if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) = +∞ )
8	7	eleq1d	⊢ ( 𝑇 = ∅ → ( if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) ∈ ℕ0 ↔ +∞ ∈ ℕ0 ) )
9		nn0re	⊢ ( +∞ ∈ ℕ0 → +∞ ∈ ℝ )
10	8 9	syl6bi	⊢ ( 𝑇 = ∅ → ( if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) ∈ ℕ0 → +∞ ∈ ℝ ) )
11	6 10	mtoi	⊢ ( 𝑇 = ∅ → ¬ if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) ∈ ℕ0 )
12	11	necon2ai	⊢ ( if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) ∈ ℕ0 → 𝑇 ≠ ∅ )
13	4 12	syl6bi	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 → 𝑇 ≠ ∅ ) )
14	1 2	ramtcl	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( ( 𝑀 Ramsey 𝐹 ) ∈ 𝑇 ↔ 𝑇 ≠ ∅ ) )
15	2	ssrab3	⊢ 𝑇 ⊆ ℕ0
16	15	sseli	⊢ ( ( 𝑀 Ramsey 𝐹 ) ∈ 𝑇 → ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 )
17	14 16	syl6bir	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 𝑇 ≠ ∅ → ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 ) )
18	13 17	impbid	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 ↔ 𝑇 ≠ ∅ ) )