Theorem ramcl2lem

Description: Lemma for extended real closure of the Ramsey number function. (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	ramcl2lem	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 𝑀 Ramsey 𝐹 ) = if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) )

Proof

Step	Hyp	Ref	Expression
1		ramval.c	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
2		ramval.t	⊢ 𝑇 = { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) }
3		eqeq2	⊢ ( +∞ = if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) → ( ( 𝑀 Ramsey 𝐹 ) = +∞ ↔ ( 𝑀 Ramsey 𝐹 ) = if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) ) )
4		eqeq2	⊢ ( inf ( 𝑇 , ℝ , < ) = if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) → ( ( 𝑀 Ramsey 𝐹 ) = inf ( 𝑇 , ℝ , < ) ↔ ( 𝑀 Ramsey 𝐹 ) = if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) ) )
5	1 2	ramval	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 𝑀 Ramsey 𝐹 ) = inf ( 𝑇 , ℝ* , < ) )
6		infeq1	⊢ ( 𝑇 = ∅ → inf ( 𝑇 , ℝ* , < ) = inf ( ∅ , ℝ* , < ) )
7		xrinf0	⊢ inf ( ∅ , ℝ* , < ) = +∞
8	6 7	eqtrdi	⊢ ( 𝑇 = ∅ → inf ( 𝑇 , ℝ* , < ) = +∞ )
9	5 8	sylan9eq	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 = ∅ ) → ( 𝑀 Ramsey 𝐹 ) = +∞ )
10		df-ne	⊢ ( 𝑇 ≠ ∅ ↔ ¬ 𝑇 = ∅ )
11	5	adantr	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → ( 𝑀 Ramsey 𝐹 ) = inf ( 𝑇 , ℝ* , < ) )
12		xrltso	⊢ < Or ℝ*
13	12	a1i	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → < Or ℝ* )
14	2	ssrab3	⊢ 𝑇 ⊆ ℕ0
15		nn0ssre	⊢ ℕ0 ⊆ ℝ
16	14 15	sstri	⊢ 𝑇 ⊆ ℝ
17		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
18	14 17	sseqtri	⊢ 𝑇 ⊆ ( ℤ≥ ‘ 0 )
19	18	a1i	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → 𝑇 ⊆ ( ℤ≥ ‘ 0 ) )
20		infssuzcl	⊢ ( ( 𝑇 ⊆ ( ℤ≥ ‘ 0 ) ∧ 𝑇 ≠ ∅ ) → inf ( 𝑇 , ℝ , < ) ∈ 𝑇 )
21	19 20	sylan	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → inf ( 𝑇 , ℝ , < ) ∈ 𝑇 )
22	16 21	sseldi	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → inf ( 𝑇 , ℝ , < ) ∈ ℝ )
23	22	rexrd	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → inf ( 𝑇 , ℝ , < ) ∈ ℝ* )
24	22	adantr	⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑧 ∈ 𝑇 ) → inf ( 𝑇 , ℝ , < ) ∈ ℝ )
25	16	a1i	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → 𝑇 ⊆ ℝ )
26	25	sselda	⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑧 ∈ 𝑇 ) → 𝑧 ∈ ℝ )
27		simpr	⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑧 ∈ 𝑇 ) → 𝑧 ∈ 𝑇 )
28		infssuzle	⊢ ( ( 𝑇 ⊆ ( ℤ≥ ‘ 0 ) ∧ 𝑧 ∈ 𝑇 ) → inf ( 𝑇 , ℝ , < ) ≤ 𝑧 )
29	18 27 28	sylancr	⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑧 ∈ 𝑇 ) → inf ( 𝑇 , ℝ , < ) ≤ 𝑧 )
30	24 26 29	lensymd	⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑧 ∈ 𝑇 ) → ¬ 𝑧 < inf ( 𝑇 , ℝ , < ) )
31	13 23 21 30	infmin	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → inf ( 𝑇 , ℝ* , < ) = inf ( 𝑇 , ℝ , < ) )
32	11 31	eqtrd	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → ( 𝑀 Ramsey 𝐹 ) = inf ( 𝑇 , ℝ , < ) )
33	10 32	sylan2br	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ¬ 𝑇 = ∅ ) → ( 𝑀 Ramsey 𝐹 ) = inf ( 𝑇 , ℝ , < ) )
34	3 4 9 33	ifbothda	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 𝑀 Ramsey 𝐹 ) = if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) )