| Step | Hyp | Ref
| Expression |
| 1 | | ffn 6736 |
. . . . . . . 8
⊢ (𝐹:𝑅⟶ℕ0 → 𝐹 Fn 𝑅) |
| 2 | | dffn4 6826 |
. . . . . . . 8
⊢ (𝐹 Fn 𝑅 ↔ 𝐹:𝑅–onto→ran 𝐹) |
| 3 | 1, 2 | sylib 218 |
. . . . . . 7
⊢ (𝐹:𝑅⟶ℕ0 → 𝐹:𝑅–onto→ran 𝐹) |
| 4 | 3 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑅 ∈ Fin ∧ 𝐹:𝑅⟶ℕ0) ∧ 𝑅 = ∅) → 𝐹:𝑅–onto→ran 𝐹) |
| 5 | | foeq2 6817 |
. . . . . . 7
⊢ (𝑅 = ∅ → (𝐹:𝑅–onto→ran 𝐹 ↔ 𝐹:∅–onto→ran 𝐹)) |
| 6 | 5 | adantl 481 |
. . . . . 6
⊢ (((𝑅 ∈ Fin ∧ 𝐹:𝑅⟶ℕ0) ∧ 𝑅 = ∅) → (𝐹:𝑅–onto→ran 𝐹 ↔ 𝐹:∅–onto→ran 𝐹)) |
| 7 | 4, 6 | mpbid 232 |
. . . . 5
⊢ (((𝑅 ∈ Fin ∧ 𝐹:𝑅⟶ℕ0) ∧ 𝑅 = ∅) → 𝐹:∅–onto→ran 𝐹) |
| 8 | | fo00 6884 |
. . . . . 6
⊢ (𝐹:∅–onto→ran 𝐹 ↔ (𝐹 = ∅ ∧ ran 𝐹 = ∅)) |
| 9 | 8 | simplbi 497 |
. . . . 5
⊢ (𝐹:∅–onto→ran 𝐹 → 𝐹 = ∅) |
| 10 | 7, 9 | syl 17 |
. . . 4
⊢ (((𝑅 ∈ Fin ∧ 𝐹:𝑅⟶ℕ0) ∧ 𝑅 = ∅) → 𝐹 = ∅) |
| 11 | 10 | oveq2d 7447 |
. . 3
⊢ (((𝑅 ∈ Fin ∧ 𝐹:𝑅⟶ℕ0) ∧ 𝑅 = ∅) → (0 Ramsey
𝐹) = (0 Ramsey
∅)) |
| 12 | | 0nn0 12541 |
. . . . 5
⊢ 0 ∈
ℕ0 |
| 13 | | ram0 17060 |
. . . . 5
⊢ (0 ∈
ℕ0 → (0 Ramsey ∅) = 0) |
| 14 | 12, 13 | ax-mp 5 |
. . . 4
⊢ (0 Ramsey
∅) = 0 |
| 15 | 14, 12 | eqeltri 2837 |
. . 3
⊢ (0 Ramsey
∅) ∈ ℕ0 |
| 16 | 11, 15 | eqeltrdi 2849 |
. 2
⊢ (((𝑅 ∈ Fin ∧ 𝐹:𝑅⟶ℕ0) ∧ 𝑅 = ∅) → (0 Ramsey
𝐹) ∈
ℕ0) |
| 17 | | 0ram2 17059 |
. . . . 5
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) → (0
Ramsey 𝐹) = sup(ran 𝐹, ℝ, <
)) |
| 18 | | frn 6743 |
. . . . . . 7
⊢ (𝐹:𝑅⟶ℕ0 → ran 𝐹 ⊆
ℕ0) |
| 19 | 18 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) → ran
𝐹 ⊆
ℕ0) |
| 20 | | nn0ssz 12636 |
. . . . . . . 8
⊢
ℕ0 ⊆ ℤ |
| 21 | 19, 20 | sstrdi 3996 |
. . . . . . 7
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) → ran
𝐹 ⊆
ℤ) |
| 22 | | fdm 6745 |
. . . . . . . . . 10
⊢ (𝐹:𝑅⟶ℕ0 → dom 𝐹 = 𝑅) |
| 23 | 22 | 3ad2ant3 1136 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) → dom
𝐹 = 𝑅) |
| 24 | | simp2 1138 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) → 𝑅 ≠ ∅) |
| 25 | 23, 24 | eqnetrd 3008 |
. . . . . . . 8
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) → dom
𝐹 ≠
∅) |
| 26 | | dm0rn0 5935 |
. . . . . . . . 9
⊢ (dom
𝐹 = ∅ ↔ ran
𝐹 =
∅) |
| 27 | 26 | necon3bii 2993 |
. . . . . . . 8
⊢ (dom
𝐹 ≠ ∅ ↔ ran
𝐹 ≠
∅) |
| 28 | 25, 27 | sylib 218 |
. . . . . . 7
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) → ran
𝐹 ≠
∅) |
| 29 | | nn0ssre 12530 |
. . . . . . . . . 10
⊢
ℕ0 ⊆ ℝ |
| 30 | 19, 29 | sstrdi 3996 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) → ran
𝐹 ⊆
ℝ) |
| 31 | | simp1 1137 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) → 𝑅 ∈ Fin) |
| 32 | 3 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) → 𝐹:𝑅–onto→ran 𝐹) |
| 33 | | fofi 9351 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Fin ∧ 𝐹:𝑅–onto→ran 𝐹) → ran 𝐹 ∈ Fin) |
| 34 | 31, 32, 33 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) → ran
𝐹 ∈
Fin) |
| 35 | | fimaxre 12212 |
. . . . . . . . 9
⊢ ((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ∈ Fin ∧ ran
𝐹 ≠ ∅) →
∃𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) |
| 36 | 30, 34, 28, 35 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) →
∃𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) |
| 37 | | ssrexv 4053 |
. . . . . . . 8
⊢ (ran
𝐹 ⊆ ℤ →
(∃𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥)) |
| 38 | 21, 36, 37 | sylc 65 |
. . . . . . 7
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) →
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) |
| 39 | | suprzcl2 12980 |
. . . . . . 7
⊢ ((ran
𝐹 ⊆ ℤ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹) |
| 40 | 21, 28, 38, 39 | syl3anc 1373 |
. . . . . 6
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) → sup(ran
𝐹, ℝ, < ) ∈
ran 𝐹) |
| 41 | 19, 40 | sseldd 3984 |
. . . . 5
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) → sup(ran
𝐹, ℝ, < ) ∈
ℕ0) |
| 42 | 17, 41 | eqeltrd 2841 |
. . . 4
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) → (0
Ramsey 𝐹) ∈
ℕ0) |
| 43 | 42 | 3expa 1119 |
. . 3
⊢ (((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅) ∧ 𝐹:𝑅⟶ℕ0) → (0
Ramsey 𝐹) ∈
ℕ0) |
| 44 | 43 | an32s 652 |
. 2
⊢ (((𝑅 ∈ Fin ∧ 𝐹:𝑅⟶ℕ0) ∧ 𝑅 ≠ ∅) → (0 Ramsey
𝐹) ∈
ℕ0) |
| 45 | 16, 44 | pm2.61dane 3029 |
1
⊢ ((𝑅 ∈ Fin ∧ 𝐹:𝑅⟶ℕ0) → (0
Ramsey 𝐹) ∈
ℕ0) |