Step | Hyp | Ref
| Expression |
1 | | eqid 2800 |
. . 3
⊢ (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖}) = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖}) |
2 | | id 22 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℕ0) |
3 | | 0ex 4985 |
. . . 4
⊢ ∅
∈ V |
4 | 3 | a1i 11 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ ∅ ∈ V) |
5 | | f0 6302 |
. . . 4
⊢
∅:∅⟶ℕ0 |
6 | 5 | a1i 11 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ ∅:∅⟶ℕ0) |
7 | | f00 6303 |
. . . . 5
⊢ (𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀)⟶∅ ↔ (𝑓 = ∅ ∧ (𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀) = ∅)) |
8 | | vex 3389 |
. . . . . . . . . 10
⊢ 𝑠 ∈ V |
9 | | simpl 475 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) →
𝑀 ∈
ℕ0) |
10 | 1 | hashbcval 16038 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ V ∧ 𝑀 ∈ ℕ0)
→ (𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀) = {𝑥 ∈ 𝒫 𝑠 ∣ (♯‘𝑥) = 𝑀}) |
11 | 8, 9, 10 | sylancr 582 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) →
(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀) = {𝑥 ∈ 𝒫 𝑠 ∣ (♯‘𝑥) = 𝑀}) |
12 | | hashfz1 13385 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ0
→ (♯‘(1...𝑀)) = 𝑀) |
13 | 12 | breq1d 4854 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ0
→ ((♯‘(1...𝑀)) ≤ (♯‘𝑠) ↔ 𝑀 ≤ (♯‘𝑠))) |
14 | 13 | biimpar 470 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) →
(♯‘(1...𝑀))
≤ (♯‘𝑠)) |
15 | | fzfid 13026 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) →
(1...𝑀) ∈
Fin) |
16 | | hashdom 13417 |
. . . . . . . . . . . . . . 15
⊢
(((1...𝑀) ∈ Fin
∧ 𝑠 ∈ V) →
((♯‘(1...𝑀))
≤ (♯‘𝑠)
↔ (1...𝑀) ≼
𝑠)) |
17 | 15, 8, 16 | sylancl 581 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) →
((♯‘(1...𝑀))
≤ (♯‘𝑠)
↔ (1...𝑀) ≼
𝑠)) |
18 | 14, 17 | mpbid 224 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) →
(1...𝑀) ≼ 𝑠) |
19 | 8 | domen 8209 |
. . . . . . . . . . . . 13
⊢
((1...𝑀) ≼
𝑠 ↔ ∃𝑥((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠)) |
20 | 18, 19 | sylib 210 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) →
∃𝑥((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠)) |
21 | | simprr 790 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) ∧
((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠)) → 𝑥 ⊆ 𝑠) |
22 | | selpw 4357 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝒫 𝑠 ↔ 𝑥 ⊆ 𝑠) |
23 | 21, 22 | sylibr 226 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) ∧
((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠)) → 𝑥 ∈ 𝒫 𝑠) |
24 | | hasheni 13387 |
. . . . . . . . . . . . . . . . 17
⊢
((1...𝑀) ≈
𝑥 →
(♯‘(1...𝑀)) =
(♯‘𝑥)) |
25 | 24 | ad2antrl 720 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) ∧
((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠)) → (♯‘(1...𝑀)) = (♯‘𝑥)) |
26 | 12 | ad2antrr 718 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) ∧
((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠)) → (♯‘(1...𝑀)) = 𝑀) |
27 | 25, 26 | eqtr3d 2836 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) ∧
((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠)) → (♯‘𝑥) = 𝑀) |
28 | 23, 27 | jca 508 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) ∧
((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠)) → (𝑥 ∈ 𝒫 𝑠 ∧ (♯‘𝑥) = 𝑀)) |
29 | 28 | ex 402 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) →
(((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠) → (𝑥 ∈ 𝒫 𝑠 ∧ (♯‘𝑥) = 𝑀))) |
30 | 29 | eximdv 2013 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) →
(∃𝑥((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠) → ∃𝑥(𝑥 ∈ 𝒫 𝑠 ∧ (♯‘𝑥) = 𝑀))) |
31 | 20, 30 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) →
∃𝑥(𝑥 ∈ 𝒫 𝑠 ∧ (♯‘𝑥) = 𝑀)) |
32 | | df-rex 3096 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈
𝒫 𝑠(♯‘𝑥) = 𝑀 ↔ ∃𝑥(𝑥 ∈ 𝒫 𝑠 ∧ (♯‘𝑥) = 𝑀)) |
33 | 31, 32 | sylibr 226 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) →
∃𝑥 ∈ 𝒫
𝑠(♯‘𝑥) = 𝑀) |
34 | | rabn0 4159 |
. . . . . . . . . 10
⊢ ({𝑥 ∈ 𝒫 𝑠 ∣ (♯‘𝑥) = 𝑀} ≠ ∅ ↔ ∃𝑥 ∈ 𝒫 𝑠(♯‘𝑥) = 𝑀) |
35 | 33, 34 | sylibr 226 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) →
{𝑥 ∈ 𝒫 𝑠 ∣ (♯‘𝑥) = 𝑀} ≠ ∅) |
36 | 11, 35 | eqnetrd 3039 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) →
(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀) ≠ ∅) |
37 | 36 | neneqd 2977 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) →
¬ (𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀) = ∅) |
38 | 37 | pm2.21d 119 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) →
((𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀) = ∅ → ∃𝑐 ∈ ∅ ∃𝑥 ∈ 𝒫 𝑠((∅‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
39 | 38 | adantld 485 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) →
((𝑓 = ∅ ∧ (𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀) = ∅) → ∃𝑐 ∈ ∅ ∃𝑥 ∈ 𝒫 𝑠((∅‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
40 | 7, 39 | syl5bi 234 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤
(♯‘𝑠)) →
(𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀)⟶∅ → ∃𝑐 ∈ ∅ ∃𝑥 ∈ 𝒫 𝑠((∅‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
41 | 40 | impr 447 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ (𝑀 ≤
(♯‘𝑠) ∧
𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀)⟶∅)) → ∃𝑐 ∈ ∅ ∃𝑥 ∈ 𝒫 𝑠((∅‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀) ⊆ (◡𝑓 “ {𝑐}))) |
42 | 1, 2, 4, 6, 2, 41 | ramub 16049 |
. 2
⊢ (𝑀 ∈ ℕ0
→ (𝑀 Ramsey ∅)
≤ 𝑀) |
43 | | nnnn0 11587 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
44 | 3 | a1i 11 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ∅
∈ V) |
45 | 5 | a1i 11 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
∅:∅⟶ℕ0) |
46 | | nnm1nn0 11622 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℕ0) |
47 | | f0 6302 |
. . . . . . 7
⊢
∅:∅⟶∅ |
48 | | fzfid 13026 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ →
(1...(𝑀 − 1)) ∈
Fin) |
49 | 1 | hashbc2 16042 |
. . . . . . . . . . 11
⊢
(((1...(𝑀 −
1)) ∈ Fin ∧ 𝑀
∈ ℕ0) → (♯‘((1...(𝑀 − 1))(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀)) = ((♯‘(1...(𝑀 − 1)))C𝑀)) |
50 | 48, 43, 49 | syl2anc 580 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ →
(♯‘((1...(𝑀
− 1))(𝑎 ∈ V,
𝑖 ∈
ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀)) = ((♯‘(1...(𝑀 − 1)))C𝑀)) |
51 | | hashfz1 13385 |
. . . . . . . . . . . 12
⊢ ((𝑀 − 1) ∈
ℕ0 → (♯‘(1...(𝑀 − 1))) = (𝑀 − 1)) |
52 | 46, 51 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ →
(♯‘(1...(𝑀
− 1))) = (𝑀 −
1)) |
53 | 52 | oveq1d 6894 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ →
((♯‘(1...(𝑀
− 1)))C𝑀) = ((𝑀 − 1)C𝑀)) |
54 | | nnz 11688 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
55 | | nnre 11321 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
56 | 55 | ltm1d 11249 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) < 𝑀) |
57 | 56 | olcd 901 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (𝑀 < 0 ∨ (𝑀 − 1) < 𝑀)) |
58 | | bcval4 13346 |
. . . . . . . . . . 11
⊢ (((𝑀 − 1) ∈
ℕ0 ∧ 𝑀
∈ ℤ ∧ (𝑀
< 0 ∨ (𝑀 − 1)
< 𝑀)) → ((𝑀 − 1)C𝑀) = 0) |
59 | 46, 54, 57, 58 | syl3anc 1491 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((𝑀 − 1)C𝑀) = 0) |
60 | 50, 53, 59 | 3eqtrd 2838 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
(♯‘((1...(𝑀
− 1))(𝑎 ∈ V,
𝑖 ∈
ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀)) = 0) |
61 | | ovex 6911 |
. . . . . . . . . 10
⊢
((1...(𝑀 −
1))(𝑎 ∈ V, 𝑖 ∈ ℕ0
↦ {𝑏 ∈ 𝒫
𝑎 ∣
(♯‘𝑏) = 𝑖})𝑀) ∈ V |
62 | | hasheq0 13403 |
. . . . . . . . . 10
⊢
(((1...(𝑀 −
1))(𝑎 ∈ V, 𝑖 ∈ ℕ0
↦ {𝑏 ∈ 𝒫
𝑎 ∣
(♯‘𝑏) = 𝑖})𝑀) ∈ V →
((♯‘((1...(𝑀
− 1))(𝑎 ∈ V,
𝑖 ∈
ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀)) = 0 ↔ ((1...(𝑀 − 1))(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀) = ∅)) |
63 | 61, 62 | ax-mp 5 |
. . . . . . . . 9
⊢
((♯‘((1...(𝑀 − 1))(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀)) = 0 ↔ ((1...(𝑀 − 1))(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀) = ∅) |
64 | 60, 63 | sylib 210 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ →
((1...(𝑀 − 1))(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀) = ∅) |
65 | 64 | feq2d 6243 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
(∅:((1...(𝑀 −
1))(𝑎 ∈ V, 𝑖 ∈ ℕ0
↦ {𝑏 ∈ 𝒫
𝑎 ∣
(♯‘𝑏) = 𝑖})𝑀)⟶∅ ↔
∅:∅⟶∅)) |
66 | 47, 65 | mpbiri 250 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
∅:((1...(𝑀 −
1))(𝑎 ∈ V, 𝑖 ∈ ℕ0
↦ {𝑏 ∈ 𝒫
𝑎 ∣
(♯‘𝑏) = 𝑖})𝑀)⟶∅) |
67 | | noel 4120 |
. . . . . . . 8
⊢ ¬
𝑐 ∈
∅ |
68 | 67 | pm2.21i 117 |
. . . . . . 7
⊢ (𝑐 ∈ ∅ → ((𝑥(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀) ⊆ (◡∅ “ {𝑐}) → (♯‘𝑥) < (∅‘𝑐))) |
69 | 68 | ad2antrl 720 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ (𝑐 ∈ ∅ ∧ 𝑥 ⊆ (1...(𝑀 − 1)))) → ((𝑥(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})𝑀) ⊆ (◡∅ “ {𝑐}) → (♯‘𝑥) < (∅‘𝑐))) |
70 | 1, 43, 44, 45, 46, 66, 69 | ramlb 16055 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) < (𝑀 Ramsey
∅)) |
71 | | ramubcl 16054 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ0
∧ ∅ ∈ V ∧ ∅:∅⟶ℕ0) ∧
(𝑀 ∈
ℕ0 ∧ (𝑀 Ramsey ∅) ≤ 𝑀)) → (𝑀 Ramsey ∅) ∈
ℕ0) |
72 | 2, 4, 6, 2, 42, 71 | syl32anc 1498 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ (𝑀 Ramsey ∅)
∈ ℕ0) |
73 | 43, 72 | syl 17 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (𝑀 Ramsey ∅) ∈
ℕ0) |
74 | | nn0lem1lt 11731 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ (𝑀 Ramsey ∅)
∈ ℕ0) → (𝑀 ≤ (𝑀 Ramsey ∅) ↔ (𝑀 − 1) < (𝑀 Ramsey ∅))) |
75 | 43, 73, 74 | syl2anc 580 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (𝑀 ≤ (𝑀 Ramsey ∅) ↔ (𝑀 − 1) < (𝑀 Ramsey ∅))) |
76 | 70, 75 | mpbird 249 |
. . . 4
⊢ (𝑀 ∈ ℕ → 𝑀 ≤ (𝑀 Ramsey ∅)) |
77 | 76 | a1i 11 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ (𝑀 ∈ ℕ
→ 𝑀 ≤ (𝑀 Ramsey
∅))) |
78 | 72 | nn0ge0d 11642 |
. . . 4
⊢ (𝑀 ∈ ℕ0
→ 0 ≤ (𝑀 Ramsey
∅)) |
79 | | breq1 4847 |
. . . 4
⊢ (𝑀 = 0 → (𝑀 ≤ (𝑀 Ramsey ∅) ↔ 0 ≤ (𝑀 Ramsey
∅))) |
80 | 78, 79 | syl5ibrcom 239 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ (𝑀 = 0 → 𝑀 ≤ (𝑀 Ramsey ∅))) |
81 | | elnn0 11581 |
. . . 4
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) |
82 | 81 | biimpi 208 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) |
83 | 77, 80, 82 | mpjaod 887 |
. 2
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ≤ (𝑀 Ramsey
∅)) |
84 | 72 | nn0red 11640 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ (𝑀 Ramsey ∅)
∈ ℝ) |
85 | | nn0re 11589 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
86 | 84, 85 | letri3d 10470 |
. 2
⊢ (𝑀 ∈ ℕ0
→ ((𝑀 Ramsey ∅)
= 𝑀 ↔ ((𝑀 Ramsey ∅) ≤ 𝑀 ∧ 𝑀 ≤ (𝑀 Ramsey ∅)))) |
87 | 42, 83, 86 | mpbir2and 705 |
1
⊢ (𝑀 ∈ ℕ0
→ (𝑀 Ramsey ∅) =
𝑀) |