| Step | Hyp | Ref
| Expression |
| 1 | | elnn0 12528 |
. . 3
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) |
| 2 | | n0 4353 |
. . . . . 6
⊢ (𝑅 ≠ ∅ ↔
∃𝑐 𝑐 ∈ 𝑅) |
| 3 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) ∧ 𝑐 ∈ 𝑅) → 𝑀 ∈ ℕ) |
| 4 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) ∧ 𝑐 ∈ 𝑅) → 𝑅 ∈ 𝑉) |
| 5 | | 0nn0 12541 |
. . . . . . . . . . 11
⊢ 0 ∈
ℕ0 |
| 6 | 5 | fconst6 6798 |
. . . . . . . . . 10
⊢ (𝑅 × {0}):𝑅⟶ℕ0 |
| 7 | 6 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) ∧ 𝑐 ∈ 𝑅) → (𝑅 × {0}):𝑅⟶ℕ0) |
| 8 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) ∧ 𝑐 ∈ 𝑅) → 𝑐 ∈ 𝑅) |
| 9 | | fvconst2g 7222 |
. . . . . . . . . 10
⊢ ((0
∈ ℕ0 ∧ 𝑐 ∈ 𝑅) → ((𝑅 × {0})‘𝑐) = 0) |
| 10 | 5, 8, 9 | sylancr 587 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) ∧ 𝑐 ∈ 𝑅) → ((𝑅 × {0})‘𝑐) = 0) |
| 11 | | ramz2 17062 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ (𝑅 × {0}):𝑅⟶ℕ0) ∧ (𝑐 ∈ 𝑅 ∧ ((𝑅 × {0})‘𝑐) = 0)) → (𝑀 Ramsey (𝑅 × {0})) = 0) |
| 12 | 3, 4, 7, 8, 10, 11 | syl32anc 1380 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) ∧ 𝑐 ∈ 𝑅) → (𝑀 Ramsey (𝑅 × {0})) = 0) |
| 13 | 12 | ex 412 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → (𝑐 ∈ 𝑅 → (𝑀 Ramsey (𝑅 × {0})) = 0)) |
| 14 | 13 | exlimdv 1933 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → (∃𝑐 𝑐 ∈ 𝑅 → (𝑀 Ramsey (𝑅 × {0})) = 0)) |
| 15 | 2, 14 | biimtrid 242 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → (𝑅 ≠ ∅ → (𝑀 Ramsey (𝑅 × {0})) = 0)) |
| 16 | 15 | expimpd 453 |
. . . 4
⊢ (𝑀 ∈ ℕ → ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (𝑀 Ramsey (𝑅 × {0})) = 0)) |
| 17 | | simpl 482 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → 𝑅 ∈ 𝑉) |
| 18 | | simpr 484 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → 𝑅 ≠ ∅) |
| 19 | 6 | a1i 11 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (𝑅 × {0}):𝑅⟶ℕ0) |
| 20 | | 0z 12624 |
. . . . . . . 8
⊢ 0 ∈
ℤ |
| 21 | | elsni 4643 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {0} → 𝑦 = 0) |
| 22 | | 0le0 12367 |
. . . . . . . . . . 11
⊢ 0 ≤
0 |
| 23 | 21, 22 | eqbrtrdi 5182 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {0} → 𝑦 ≤ 0) |
| 24 | 23 | rgen 3063 |
. . . . . . . . 9
⊢
∀𝑦 ∈
{0}𝑦 ≤
0 |
| 25 | | rnxp 6190 |
. . . . . . . . . . 11
⊢ (𝑅 ≠ ∅ → ran (𝑅 × {0}) =
{0}) |
| 26 | 25 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → ran (𝑅 × {0}) = {0}) |
| 27 | 26 | raleqdv 3326 |
. . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (∀𝑦 ∈ ran (𝑅 × {0})𝑦 ≤ 0 ↔ ∀𝑦 ∈ {0}𝑦 ≤ 0)) |
| 28 | 24, 27 | mpbiri 258 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → ∀𝑦 ∈ ran (𝑅 × {0})𝑦 ≤ 0) |
| 29 | | brralrspcev 5203 |
. . . . . . . 8
⊢ ((0
∈ ℤ ∧ ∀𝑦 ∈ ran (𝑅 × {0})𝑦 ≤ 0) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ ran (𝑅 × {0})𝑦 ≤ 𝑥) |
| 30 | 20, 28, 29 | sylancr 587 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ ran (𝑅 × {0})𝑦 ≤ 𝑥) |
| 31 | | 0ram 17058 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ (𝑅 × {0}):𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran (𝑅 × {0})𝑦 ≤ 𝑥) → (0 Ramsey (𝑅 × {0})) = sup(ran (𝑅 × {0}), ℝ, <
)) |
| 32 | 17, 18, 19, 30, 31 | syl31anc 1375 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (0 Ramsey (𝑅 × {0})) = sup(ran (𝑅 × {0}), ℝ, <
)) |
| 33 | 26 | supeq1d 9486 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → sup(ran (𝑅 × {0}), ℝ, < ) =
sup({0}, ℝ, < )) |
| 34 | | ltso 11341 |
. . . . . . . 8
⊢ < Or
ℝ |
| 35 | | 0re 11263 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
| 36 | | supsn 9512 |
. . . . . . . 8
⊢ (( <
Or ℝ ∧ 0 ∈ ℝ) → sup({0}, ℝ, < ) =
0) |
| 37 | 34, 35, 36 | mp2an 692 |
. . . . . . 7
⊢ sup({0},
ℝ, < ) = 0 |
| 38 | 37 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → sup({0}, ℝ, <
) = 0) |
| 39 | 32, 33, 38 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (0 Ramsey (𝑅 × {0})) =
0) |
| 40 | | oveq1 7438 |
. . . . . 6
⊢ (𝑀 = 0 → (𝑀 Ramsey (𝑅 × {0})) = (0 Ramsey (𝑅 × {0}))) |
| 41 | 40 | eqeq1d 2739 |
. . . . 5
⊢ (𝑀 = 0 → ((𝑀 Ramsey (𝑅 × {0})) = 0 ↔ (0 Ramsey (𝑅 × {0})) =
0)) |
| 42 | 39, 41 | imbitrrid 246 |
. . . 4
⊢ (𝑀 = 0 → ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (𝑀 Ramsey (𝑅 × {0})) = 0)) |
| 43 | 16, 42 | jaoi 858 |
. . 3
⊢ ((𝑀 ∈ ℕ ∨ 𝑀 = 0) → ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (𝑀 Ramsey (𝑅 × {0})) = 0)) |
| 44 | 1, 43 | sylbi 217 |
. 2
⊢ (𝑀 ∈ ℕ0
→ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (𝑀 Ramsey (𝑅 × {0})) = 0)) |
| 45 | 44 | 3impib 1117 |
1
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (𝑀 Ramsey (𝑅 × {0})) = 0) |