Theorem 0ram2

Description: The Ramsey number when M = 0 . (Contributed by Mario Carneiro, 22-Apr-2015)

	Ref	Expression
Assertion	0ram2	⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 0 Ramsey 𝐹 ) = sup ( ran 𝐹 , ℝ , < ) )

Proof

Step	Hyp	Ref	Expression
1		frn	⊢ ( 𝐹 : 𝑅 ⟶ ℕ0 → ran 𝐹 ⊆ ℕ0 )
2	1	3ad2ant3	⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ran 𝐹 ⊆ ℕ0 )
3		nn0ssz	⊢ ℕ0 ⊆ ℤ
4	2 3	sstrdi	⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ran 𝐹 ⊆ ℤ )
5		nn0ssre	⊢ ℕ0 ⊆ ℝ
6	2 5	sstrdi	⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ran 𝐹 ⊆ ℝ )
7		simp1	⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → 𝑅 ∈ Fin )
8		ffn	⊢ ( 𝐹 : 𝑅 ⟶ ℕ0 → 𝐹 Fn 𝑅 )
9	8	3ad2ant3	⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → 𝐹 Fn 𝑅 )
10		dffn4	⊢ ( 𝐹 Fn 𝑅 ↔ 𝐹 : 𝑅 –onto→ ran 𝐹 )
11	9 10	sylib	⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → 𝐹 : 𝑅 –onto→ ran 𝐹 )
12		fofi	⊢ ( ( 𝑅 ∈ Fin ∧ 𝐹 : 𝑅 –onto→ ran 𝐹 ) → ran 𝐹 ∈ Fin )
13	7 11 12	syl2anc	⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ran 𝐹 ∈ Fin )
14		fdm	⊢ ( 𝐹 : 𝑅 ⟶ ℕ0 → dom 𝐹 = 𝑅 )
15	14	3ad2ant3	⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → dom 𝐹 = 𝑅 )
16		simp2	⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → 𝑅 ≠ ∅ )
17	15 16	eqnetrd	⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → dom 𝐹 ≠ ∅ )
18		dm0rn0	⊢ ( dom 𝐹 = ∅ ↔ ran 𝐹 = ∅ )
19	18	necon3bii	⊢ ( dom 𝐹 ≠ ∅ ↔ ran 𝐹 ≠ ∅ )
20	17 19	sylib	⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ran 𝐹 ≠ ∅ )
21		fimaxre	⊢ ( ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ∈ Fin ∧ ran 𝐹 ≠ ∅ ) → ∃ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 )
22	6 13 20 21	syl3anc	⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ∃ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 )
23		ssrexv	⊢ ( ran 𝐹 ⊆ ℤ → ( ∃ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 → ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) )
24	4 22 23	sylc	⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 )
25		0ram	⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → ( 0 Ramsey 𝐹 ) = sup ( ran 𝐹 , ℝ , < ) )
26	24 25	mpdan	⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 0 Ramsey 𝐹 ) = sup ( ran 𝐹 , ℝ , < ) )