Metamath Proof Explorer

Theorem 0ramcl

Description: Lemma for ramcl : Existence of the Ramsey number when M = 0 . (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion 0ramcl ( ( 𝑅 ∈ Fin ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 0 Ramsey 𝐹 ) ∈ ℕ0 )

Proof

Step Hyp Ref Expression
1 ffn ⊢ ( 𝐹 : 𝑅 ⟶ ℕ0 → 𝐹 Fn 𝑅 )
2 dffn4 ⊢ ( 𝐹 Fn 𝑅 ↔ 𝐹 : 𝑅 –onto→ ran 𝐹 )
3 1 2 sylib ⊢ ( 𝐹 : 𝑅 ⟶ ℕ0 → 𝐹 : 𝑅 –onto→ ran 𝐹 )
4 3 ad2antlr ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑅 = ∅ ) → 𝐹 : 𝑅 –onto→ ran 𝐹 )
5 foeq2 ⊢ ( 𝑅 = ∅ → ( 𝐹 : 𝑅 –onto→ ran 𝐹 ↔ 𝐹 : ∅ –onto→ ran 𝐹 ) )
6 5 adantl ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑅 = ∅ ) → ( 𝐹 : 𝑅 –onto→ ran 𝐹 ↔ 𝐹 : ∅ –onto→ ran 𝐹 ) )
7 4 6 mpbid ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑅 = ∅ ) → 𝐹 : ∅ –onto→ ran 𝐹 )
8 fo00 ⊢ ( 𝐹 : ∅ –onto→ ran 𝐹 ↔ ( 𝐹 = ∅ ∧ ran 𝐹 = ∅ ) )
9 8 simplbi ⊢ ( 𝐹 : ∅ –onto→ ran 𝐹 → 𝐹 = ∅ )
10 7 9 syl ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑅 = ∅ ) → 𝐹 = ∅ )
11 10 oveq2d ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑅 = ∅ ) → ( 0 Ramsey 𝐹 ) = ( 0 Ramsey ∅ ) )
12 0nn0 ⊢ 0 ∈ ℕ0
13 ram0 ⊢ ( 0 ∈ ℕ0 → ( 0 Ramsey ∅ ) = 0 )
14 12 13 ax-mp ⊢ ( 0 Ramsey ∅ ) = 0
15 14 12 eqeltri ⊢ ( 0 Ramsey ∅ ) ∈ ℕ0
16 11 15 eqeltrdi ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑅 = ∅ ) → ( 0 Ramsey 𝐹 ) ∈ ℕ0 )
17 0ram2 ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 0 Ramsey 𝐹 ) = sup ( ran 𝐹 , ℝ , < ) )
18 frn ⊢ ( 𝐹 : 𝑅 ⟶ ℕ0 → ran 𝐹 ⊆ ℕ0 )
19 18 3ad2ant3 ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ran 𝐹 ⊆ ℕ0 )
20 nn0ssz ⊢ ℕ0 ⊆ ℤ
21 19 20 sstrdi ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ran 𝐹 ⊆ ℤ )
22 fdm ⊢ ( 𝐹 : 𝑅 ⟶ ℕ0 → dom 𝐹 = 𝑅 )
23 22 3ad2ant3 ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → dom 𝐹 = 𝑅 )
24 simp2 ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → 𝑅 ≠ ∅ )
25 23 24 eqnetrd ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → dom 𝐹 ≠ ∅ )
26 dm0rn0 ⊢ ( dom 𝐹 = ∅ ↔ ran 𝐹 = ∅ )
27 26 necon3bii ⊢ ( dom 𝐹 ≠ ∅ ↔ ran 𝐹 ≠ ∅ )
28 25 27 sylib ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ran 𝐹 ≠ ∅ )
29 nn0ssre ⊢ ℕ0 ⊆ ℝ
30 19 29 sstrdi ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ran 𝐹 ⊆ ℝ )
31 simp1 ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → 𝑅 ∈ Fin )
32 3 3ad2ant3 ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → 𝐹 : 𝑅 –onto→ ran 𝐹 )
33 fofi ⊢ ( ( 𝑅 ∈ Fin ∧ 𝐹 : 𝑅 –onto→ ran 𝐹 ) → ran 𝐹 ∈ Fin )
34 31 32 33 syl2anc ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ran 𝐹 ∈ Fin )
35 fimaxre ⊢ ( ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ∈ Fin ∧ ran 𝐹 ≠ ∅ ) → ∃ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 )
36 30 34 28 35 syl3anc ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ∃ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 )
37 ssrexv ⊢ ( ran 𝐹 ⊆ ℤ → ( ∃ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 → ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) )
38 21 36 37 sylc ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 )
39 suprzcl2 ⊢ ( ( ran 𝐹 ⊆ ℤ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 )
40 21 28 38 39 syl3anc ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 )
41 19 40 sseldd ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℕ0 )
42 17 41 eqeltrd ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 0 Ramsey 𝐹 ) ∈ ℕ0 )
43 42 3expa ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ) ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 0 Ramsey 𝐹 ) ∈ ℕ0 )
44 43 an32s ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑅 ≠ ∅ ) → ( 0 Ramsey 𝐹 ) ∈ ℕ0 )
45 16 44 pm2.61dane ⊢ ( ( 𝑅 ∈ Fin ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 0 Ramsey 𝐹 ) ∈ ℕ0 )