Step | Hyp | Ref
| Expression |
1 | | elnn0 11294 |
. . 3
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) |
2 | | n0 3931 |
. . . . . 6
⊢ (𝑅 ≠ ∅ ↔
∃𝑐 𝑐 ∈ 𝑅) |
3 | | simpll 790 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) ∧ 𝑐 ∈ 𝑅) → 𝑀 ∈ ℕ) |
4 | | simplr 792 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) ∧ 𝑐 ∈ 𝑅) → 𝑅 ∈ 𝑉) |
5 | | 0nn0 11307 |
. . . . . . . . . . 11
⊢ 0 ∈
ℕ0 |
6 | 5 | fconst6 6095 |
. . . . . . . . . 10
⊢ (𝑅 × {0}):𝑅⟶ℕ0 |
7 | 6 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) ∧ 𝑐 ∈ 𝑅) → (𝑅 × {0}):𝑅⟶ℕ0) |
8 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) ∧ 𝑐 ∈ 𝑅) → 𝑐 ∈ 𝑅) |
9 | | fvconst2g 6467 |
. . . . . . . . . 10
⊢ ((0
∈ ℕ0 ∧ 𝑐 ∈ 𝑅) → ((𝑅 × {0})‘𝑐) = 0) |
10 | 5, 8, 9 | sylancr 695 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) ∧ 𝑐 ∈ 𝑅) → ((𝑅 × {0})‘𝑐) = 0) |
11 | | ramz2 15728 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ (𝑅 × {0}):𝑅⟶ℕ0) ∧ (𝑐 ∈ 𝑅 ∧ ((𝑅 × {0})‘𝑐) = 0)) → (𝑀 Ramsey (𝑅 × {0})) = 0) |
12 | 3, 4, 7, 8, 10, 11 | syl32anc 1334 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) ∧ 𝑐 ∈ 𝑅) → (𝑀 Ramsey (𝑅 × {0})) = 0) |
13 | 12 | ex 450 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → (𝑐 ∈ 𝑅 → (𝑀 Ramsey (𝑅 × {0})) = 0)) |
14 | 13 | exlimdv 1861 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → (∃𝑐 𝑐 ∈ 𝑅 → (𝑀 Ramsey (𝑅 × {0})) = 0)) |
15 | 2, 14 | syl5bi 232 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → (𝑅 ≠ ∅ → (𝑀 Ramsey (𝑅 × {0})) = 0)) |
16 | 15 | expimpd 629 |
. . . 4
⊢ (𝑀 ∈ ℕ → ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (𝑀 Ramsey (𝑅 × {0})) = 0)) |
17 | | simpl 473 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → 𝑅 ∈ 𝑉) |
18 | | simpr 477 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → 𝑅 ≠ ∅) |
19 | 6 | a1i 11 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (𝑅 × {0}):𝑅⟶ℕ0) |
20 | | 0z 11388 |
. . . . . . . 8
⊢ 0 ∈
ℤ |
21 | | elsni 4194 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {0} → 𝑦 = 0) |
22 | | 0le0 11110 |
. . . . . . . . . . 11
⊢ 0 ≤
0 |
23 | 21, 22 | syl6eqbr 4692 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {0} → 𝑦 ≤ 0) |
24 | 23 | rgen 2922 |
. . . . . . . . 9
⊢
∀𝑦 ∈
{0}𝑦 ≤
0 |
25 | | rnxp 5564 |
. . . . . . . . . . 11
⊢ (𝑅 ≠ ∅ → ran (𝑅 × {0}) =
{0}) |
26 | 25 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → ran (𝑅 × {0}) = {0}) |
27 | 26 | raleqdv 3144 |
. . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (∀𝑦 ∈ ran (𝑅 × {0})𝑦 ≤ 0 ↔ ∀𝑦 ∈ {0}𝑦 ≤ 0)) |
28 | 24, 27 | mpbiri 248 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → ∀𝑦 ∈ ran (𝑅 × {0})𝑦 ≤ 0) |
29 | | breq2 4657 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 0)) |
30 | 29 | ralbidv 2986 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (∀𝑦 ∈ ran (𝑅 × {0})𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ ran (𝑅 × {0})𝑦 ≤ 0)) |
31 | 30 | rspcev 3309 |
. . . . . . . 8
⊢ ((0
∈ ℤ ∧ ∀𝑦 ∈ ran (𝑅 × {0})𝑦 ≤ 0) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ ran (𝑅 × {0})𝑦 ≤ 𝑥) |
32 | 20, 28, 31 | sylancr 695 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ ran (𝑅 × {0})𝑦 ≤ 𝑥) |
33 | | 0ram 15724 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ (𝑅 × {0}):𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran (𝑅 × {0})𝑦 ≤ 𝑥) → (0 Ramsey (𝑅 × {0})) = sup(ran (𝑅 × {0}), ℝ, <
)) |
34 | 17, 18, 19, 32, 33 | syl31anc 1329 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (0 Ramsey (𝑅 × {0})) = sup(ran (𝑅 × {0}), ℝ, <
)) |
35 | 26 | supeq1d 8352 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → sup(ran (𝑅 × {0}), ℝ, < ) =
sup({0}, ℝ, < )) |
36 | | ltso 10118 |
. . . . . . . 8
⊢ < Or
ℝ |
37 | | 0re 10040 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
38 | | supsn 8378 |
. . . . . . . 8
⊢ (( <
Or ℝ ∧ 0 ∈ ℝ) → sup({0}, ℝ, < ) =
0) |
39 | 36, 37, 38 | mp2an 708 |
. . . . . . 7
⊢ sup({0},
ℝ, < ) = 0 |
40 | 39 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → sup({0}, ℝ, <
) = 0) |
41 | 34, 35, 40 | 3eqtrd 2660 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (0 Ramsey (𝑅 × {0})) =
0) |
42 | | oveq1 6657 |
. . . . . 6
⊢ (𝑀 = 0 → (𝑀 Ramsey (𝑅 × {0})) = (0 Ramsey (𝑅 × {0}))) |
43 | 42 | eqeq1d 2624 |
. . . . 5
⊢ (𝑀 = 0 → ((𝑀 Ramsey (𝑅 × {0})) = 0 ↔ (0 Ramsey (𝑅 × {0})) =
0)) |
44 | 41, 43 | syl5ibr 236 |
. . . 4
⊢ (𝑀 = 0 → ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (𝑀 Ramsey (𝑅 × {0})) = 0)) |
45 | 16, 44 | jaoi 394 |
. . 3
⊢ ((𝑀 ∈ ℕ ∨ 𝑀 = 0) → ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (𝑀 Ramsey (𝑅 × {0})) = 0)) |
46 | 1, 45 | sylbi 207 |
. 2
⊢ (𝑀 ∈ ℕ0
→ ((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (𝑀 Ramsey (𝑅 × {0})) = 0)) |
47 | 46 | 3impib 1262 |
1
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (𝑀 Ramsey (𝑅 × {0})) = 0) |