Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢ (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖}) = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖}) |
2 | | id 22 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℕ0) |
3 | | 0ex 4790 |
. . . 4
⊢ ∅
∈ V |
4 | 3 | a1i 11 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ ∅ ∈ V) |
5 | | f0 6086 |
. . . 4
⊢
∅:∅⟶ℕ0 |
6 | 5 | a1i 11 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ ∅:∅⟶ℕ0) |
7 | | f00 6087 |
. . . . 5
⊢ (𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶∅ ↔ (𝑓 = ∅ ∧ (𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) = ∅)) |
8 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑠 ∈ V |
9 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) → 𝑀 ∈
ℕ0) |
10 | 1 | hashbcval 15706 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ V ∧ 𝑀 ∈ ℕ0)
→ (𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) = {𝑥 ∈ 𝒫 𝑠 ∣ (#‘𝑥) = 𝑀}) |
11 | 8, 9, 10 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) → (𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) = {𝑥 ∈ 𝒫 𝑠 ∣ (#‘𝑥) = 𝑀}) |
12 | | hashfz1 13134 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ0
→ (#‘(1...𝑀)) =
𝑀) |
13 | 12 | breq1d 4663 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ0
→ ((#‘(1...𝑀))
≤ (#‘𝑠) ↔
𝑀 ≤ (#‘𝑠))) |
14 | 13 | biimpar 502 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) → (#‘(1...𝑀)) ≤ (#‘𝑠)) |
15 | | fzfid 12772 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) → (1...𝑀) ∈ Fin) |
16 | | hashdom 13168 |
. . . . . . . . . . . . . . 15
⊢
(((1...𝑀) ∈ Fin
∧ 𝑠 ∈ V) →
((#‘(1...𝑀)) ≤
(#‘𝑠) ↔
(1...𝑀) ≼ 𝑠)) |
17 | 15, 8, 16 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) → ((#‘(1...𝑀)) ≤ (#‘𝑠) ↔ (1...𝑀) ≼ 𝑠)) |
18 | 14, 17 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) → (1...𝑀) ≼ 𝑠) |
19 | 8 | domen 7968 |
. . . . . . . . . . . . 13
⊢
((1...𝑀) ≼
𝑠 ↔ ∃𝑥((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠)) |
20 | 18, 19 | sylib 208 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) → ∃𝑥((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠)) |
21 | | simprr 796 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) ∧ ((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠)) → 𝑥 ⊆ 𝑠) |
22 | | selpw 4165 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝒫 𝑠 ↔ 𝑥 ⊆ 𝑠) |
23 | 21, 22 | sylibr 224 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) ∧ ((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠)) → 𝑥 ∈ 𝒫 𝑠) |
24 | | hasheni 13136 |
. . . . . . . . . . . . . . . . 17
⊢
((1...𝑀) ≈
𝑥 →
(#‘(1...𝑀)) =
(#‘𝑥)) |
25 | 24 | ad2antrl 764 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) ∧ ((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠)) → (#‘(1...𝑀)) = (#‘𝑥)) |
26 | 12 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) ∧ ((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠)) → (#‘(1...𝑀)) = 𝑀) |
27 | 25, 26 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) ∧ ((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠)) → (#‘𝑥) = 𝑀) |
28 | 23, 27 | jca 554 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) ∧ ((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠)) → (𝑥 ∈ 𝒫 𝑠 ∧ (#‘𝑥) = 𝑀)) |
29 | 28 | ex 450 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) → (((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠) → (𝑥 ∈ 𝒫 𝑠 ∧ (#‘𝑥) = 𝑀))) |
30 | 29 | eximdv 1846 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) → (∃𝑥((1...𝑀) ≈ 𝑥 ∧ 𝑥 ⊆ 𝑠) → ∃𝑥(𝑥 ∈ 𝒫 𝑠 ∧ (#‘𝑥) = 𝑀))) |
31 | 20, 30 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) → ∃𝑥(𝑥 ∈ 𝒫 𝑠 ∧ (#‘𝑥) = 𝑀)) |
32 | | df-rex 2918 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈
𝒫 𝑠(#‘𝑥) = 𝑀 ↔ ∃𝑥(𝑥 ∈ 𝒫 𝑠 ∧ (#‘𝑥) = 𝑀)) |
33 | 31, 32 | sylibr 224 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) → ∃𝑥 ∈ 𝒫 𝑠(#‘𝑥) = 𝑀) |
34 | | rabn0 3958 |
. . . . . . . . . 10
⊢ ({𝑥 ∈ 𝒫 𝑠 ∣ (#‘𝑥) = 𝑀} ≠ ∅ ↔ ∃𝑥 ∈ 𝒫 𝑠(#‘𝑥) = 𝑀) |
35 | 33, 34 | sylibr 224 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) → {𝑥 ∈ 𝒫 𝑠 ∣ (#‘𝑥) = 𝑀} ≠ ∅) |
36 | 11, 35 | eqnetrd 2861 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) → (𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) ≠ ∅) |
37 | 36 | neneqd 2799 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) → ¬ (𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) = ∅) |
38 | 37 | pm2.21d 118 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) → ((𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) = ∅ → ∃𝑐 ∈ ∅ ∃𝑥 ∈ 𝒫 𝑠((∅‘𝑐) ≤ (#‘𝑥) ∧ (𝑥(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
39 | 38 | adantld 483 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) → ((𝑓 = ∅ ∧ (𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) = ∅) → ∃𝑐 ∈ ∅ ∃𝑥 ∈ 𝒫 𝑠((∅‘𝑐) ≤ (#‘𝑥) ∧ (𝑥(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
40 | 7, 39 | syl5bi 232 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (#‘𝑠)) → (𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶∅ → ∃𝑐 ∈ ∅ ∃𝑥 ∈ 𝒫 𝑠((∅‘𝑐) ≤ (#‘𝑥) ∧ (𝑥(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
41 | 40 | impr 649 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ (𝑀 ≤
(#‘𝑠) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶∅)) → ∃𝑐 ∈ ∅ ∃𝑥 ∈ 𝒫 𝑠((∅‘𝑐) ≤ (#‘𝑥) ∧ (𝑥(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) ⊆ (◡𝑓 “ {𝑐}))) |
42 | 1, 2, 4, 6, 2, 41 | ramub 15717 |
. 2
⊢ (𝑀 ∈ ℕ0
→ (𝑀 Ramsey ∅)
≤ 𝑀) |
43 | | nnnn0 11299 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
44 | 3 | a1i 11 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ∅
∈ V) |
45 | 5 | a1i 11 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
∅:∅⟶ℕ0) |
46 | | nnm1nn0 11334 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℕ0) |
47 | | f0 6086 |
. . . . . . 7
⊢
∅:∅⟶∅ |
48 | | fzfid 12772 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ →
(1...(𝑀 − 1)) ∈
Fin) |
49 | 1 | hashbc2 15710 |
. . . . . . . . . . 11
⊢
(((1...(𝑀 −
1)) ∈ Fin ∧ 𝑀
∈ ℕ0) → (#‘((1...(𝑀 − 1))(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)) = ((#‘(1...(𝑀 − 1)))C𝑀)) |
50 | 48, 43, 49 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ →
(#‘((1...(𝑀 −
1))(𝑎 ∈ V, 𝑖 ∈ ℕ0
↦ {𝑏 ∈ 𝒫
𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)) = ((#‘(1...(𝑀 − 1)))C𝑀)) |
51 | | hashfz1 13134 |
. . . . . . . . . . . 12
⊢ ((𝑀 − 1) ∈
ℕ0 → (#‘(1...(𝑀 − 1))) = (𝑀 − 1)) |
52 | 46, 51 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ →
(#‘(1...(𝑀 −
1))) = (𝑀 −
1)) |
53 | 52 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ →
((#‘(1...(𝑀 −
1)))C𝑀) = ((𝑀 − 1)C𝑀)) |
54 | | nnz 11399 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
55 | | nnre 11027 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
56 | 55 | ltm1d 10956 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) < 𝑀) |
57 | 56 | olcd 408 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (𝑀 < 0 ∨ (𝑀 − 1) < 𝑀)) |
58 | | bcval4 13094 |
. . . . . . . . . . 11
⊢ (((𝑀 − 1) ∈
ℕ0 ∧ 𝑀
∈ ℤ ∧ (𝑀
< 0 ∨ (𝑀 − 1)
< 𝑀)) → ((𝑀 − 1)C𝑀) = 0) |
59 | 46, 54, 57, 58 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((𝑀 − 1)C𝑀) = 0) |
60 | 50, 53, 59 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
(#‘((1...(𝑀 −
1))(𝑎 ∈ V, 𝑖 ∈ ℕ0
↦ {𝑏 ∈ 𝒫
𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)) = 0) |
61 | | ovex 6678 |
. . . . . . . . . 10
⊢
((1...(𝑀 −
1))(𝑎 ∈ V, 𝑖 ∈ ℕ0
↦ {𝑏 ∈ 𝒫
𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) ∈ V |
62 | | hasheq0 13154 |
. . . . . . . . . 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 208 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ →
((1...(𝑀 − 1))(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) = ∅) |
65 | 64 | feq2d 6031 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
(∅:((1...(𝑀 −
1))(𝑎 ∈ V, 𝑖 ∈ ℕ0
↦ {𝑏 ∈ 𝒫
𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶∅ ↔
∅:∅⟶∅)) |
66 | 47, 65 | mpbiri 248 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
∅:((1...(𝑀 −
1))(𝑎 ∈ V, 𝑖 ∈ ℕ0
↦ {𝑏 ∈ 𝒫
𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶∅) |
67 | | noel 3919 |
. . . . . . . 8
⊢ ¬
𝑐 ∈
∅ |
68 | 67 | pm2.21i 116 |
. . . . . . 7
⊢ (𝑐 ∈ ∅ → ((𝑥(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) ⊆ (◡∅ “ {𝑐}) → (#‘𝑥) < (∅‘𝑐))) |
69 | 68 | ad2antrl 764 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ (𝑐 ∈ ∅ ∧ 𝑥 ⊆ (1...(𝑀 − 1)))) → ((𝑥(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) ⊆ (◡∅ “ {𝑐}) → (#‘𝑥) < (∅‘𝑐))) |
70 | 1, 43, 44, 45, 46, 66, 69 | ramlb 15723 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) < (𝑀 Ramsey
∅)) |
71 | | ramubcl 15722 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ0
∧ ∅ ∈ V ∧ ∅:∅⟶ℕ0) ∧
(𝑀 ∈
ℕ0 ∧ (𝑀 Ramsey ∅) ≤ 𝑀)) → (𝑀 Ramsey ∅) ∈
ℕ0) |
72 | 2, 4, 6, 2, 42, 71 | syl32anc 1334 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ (𝑀 Ramsey ∅)
∈ ℕ0) |
73 | 43, 72 | syl 17 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (𝑀 Ramsey ∅) ∈
ℕ0) |
74 | | nn0lem1lt 11442 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ (𝑀 Ramsey ∅)
∈ ℕ0) → (𝑀 ≤ (𝑀 Ramsey ∅) ↔ (𝑀 − 1) < (𝑀 Ramsey ∅))) |
75 | 43, 73, 74 | syl2anc 693 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (𝑀 ≤ (𝑀 Ramsey ∅) ↔ (𝑀 − 1) < (𝑀 Ramsey ∅))) |
76 | 70, 75 | mpbird 247 |
. . . 4
⊢ (𝑀 ∈ ℕ → 𝑀 ≤ (𝑀 Ramsey ∅)) |
77 | 76 | a1i 11 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ (𝑀 ∈ ℕ
→ 𝑀 ≤ (𝑀 Ramsey
∅))) |
78 | 72 | nn0ge0d 11354 |
. . . 4
⊢ (𝑀 ∈ ℕ0
→ 0 ≤ (𝑀 Ramsey
∅)) |
79 | | breq1 4656 |
. . . 4
⊢ (𝑀 = 0 → (𝑀 ≤ (𝑀 Ramsey ∅) ↔ 0 ≤ (𝑀 Ramsey
∅))) |
80 | 78, 79 | syl5ibrcom 237 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ (𝑀 = 0 → 𝑀 ≤ (𝑀 Ramsey ∅))) |
81 | | elnn0 11294 |
. . . 4
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) |
82 | 81 | biimpi 206 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) |
83 | 77, 80, 82 | mpjaod 396 |
. 2
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ≤ (𝑀 Ramsey
∅)) |
84 | 72 | nn0red 11352 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ (𝑀 Ramsey ∅)
∈ ℝ) |
85 | | nn0re 11301 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
86 | 84, 85 | letri3d 10179 |
. 2
⊢ (𝑀 ∈ ℕ0
→ ((𝑀 Ramsey ∅)
= 𝑀 ↔ ((𝑀 Ramsey ∅) ≤ 𝑀 ∧ 𝑀 ≤ (𝑀 Ramsey ∅)))) |
87 | 42, 83, 86 | mpbir2and 957 |
1
⊢ (𝑀 ∈ ℕ0
→ (𝑀 Ramsey ∅) =
𝑀) |