Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. 2
⊢ (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖}) = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖}) |
2 | | ramub1.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℕ) |
3 | 2 | nnnn0d 11228 |
. 2
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
4 | | ramub1.r |
. 2
⊢ (𝜑 → 𝑅 ∈ Fin) |
5 | | ramub1.f |
. . 3
⊢ (𝜑 → 𝐹:𝑅⟶ℕ) |
6 | | nnssnn0 11172 |
. . 3
⊢ ℕ
⊆ ℕ0 |
7 | | fss 5969 |
. . 3
⊢ ((𝐹:𝑅⟶ℕ ∧ ℕ ⊆
ℕ0) → 𝐹:𝑅⟶ℕ0) |
8 | 5, 6, 7 | sylancl 693 |
. 2
⊢ (𝜑 → 𝐹:𝑅⟶ℕ0) |
9 | | ramub1.2 |
. . 3
⊢ (𝜑 → ((𝑀 − 1) Ramsey 𝐺) ∈
ℕ0) |
10 | | peano2nn0 11210 |
. . 3
⊢ (((𝑀 − 1) Ramsey 𝐺) ∈ ℕ0
→ (((𝑀 − 1)
Ramsey 𝐺) + 1) ∈
ℕ0) |
11 | 9, 10 | syl 17 |
. 2
⊢ (𝜑 → (((𝑀 − 1) Ramsey 𝐺) + 1) ∈
ℕ0) |
12 | | simprl 790 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅)) → (#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1)) |
13 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅)) → ((𝑀 − 1) Ramsey 𝐺) ∈
ℕ0) |
14 | | nn0p1nn 11209 |
. . . . . . 7
⊢ (((𝑀 − 1) Ramsey 𝐺) ∈ ℕ0
→ (((𝑀 − 1)
Ramsey 𝐺) + 1) ∈
ℕ) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅)) → (((𝑀 − 1) Ramsey 𝐺) + 1) ∈ ℕ) |
16 | 12, 15 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ ((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅)) → (#‘𝑠) ∈ ℕ) |
17 | 16 | nnnn0d 11228 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅)) → (#‘𝑠) ∈
ℕ0) |
18 | | vex 3176 |
. . . . . . . 8
⊢ 𝑠 ∈ V |
19 | | hashclb 13011 |
. . . . . . . 8
⊢ (𝑠 ∈ V → (𝑠 ∈ Fin ↔
(#‘𝑠) ∈
ℕ0)) |
20 | 18, 19 | ax-mp 5 |
. . . . . . 7
⊢ (𝑠 ∈ Fin ↔
(#‘𝑠) ∈
ℕ0) |
21 | 17, 20 | sylibr 223 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅)) → 𝑠 ∈ Fin) |
22 | | hashnncl 13018 |
. . . . . 6
⊢ (𝑠 ∈ Fin →
((#‘𝑠) ∈ ℕ
↔ 𝑠 ≠
∅)) |
23 | 21, 22 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ ((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅)) → ((#‘𝑠) ∈ ℕ ↔ 𝑠 ≠ ∅)) |
24 | 16, 23 | mpbid 221 |
. . . 4
⊢ ((𝜑 ∧ ((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅)) → 𝑠 ≠ ∅) |
25 | | n0 3890 |
. . . 4
⊢ (𝑠 ≠ ∅ ↔
∃𝑤 𝑤 ∈ 𝑠) |
26 | 24, 25 | sylib 207 |
. . 3
⊢ ((𝜑 ∧ ((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅)) → ∃𝑤 𝑤 ∈ 𝑠) |
27 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅) ∧ 𝑤 ∈ 𝑠)) → 𝑀 ∈ ℕ) |
28 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅) ∧ 𝑤 ∈ 𝑠)) → 𝑅 ∈ Fin) |
29 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅) ∧ 𝑤 ∈ 𝑠)) → 𝐹:𝑅⟶ℕ) |
30 | | ramub1.g |
. . . . . 6
⊢ 𝐺 = (𝑥 ∈ 𝑅 ↦ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝐹‘𝑥) − 1), (𝐹‘𝑦))))) |
31 | | ramub1.1 |
. . . . . . 7
⊢ (𝜑 → 𝐺:𝑅⟶ℕ0) |
32 | 31 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅) ∧ 𝑤 ∈ 𝑠)) → 𝐺:𝑅⟶ℕ0) |
33 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅) ∧ 𝑤 ∈ 𝑠)) → ((𝑀 − 1) Ramsey 𝐺) ∈
ℕ0) |
34 | 21 | adantrr 749 |
. . . . . 6
⊢ ((𝜑 ∧ (((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅) ∧ 𝑤 ∈ 𝑠)) → 𝑠 ∈ Fin) |
35 | | simprll 798 |
. . . . . 6
⊢ ((𝜑 ∧ (((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅) ∧ 𝑤 ∈ 𝑠)) → (#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1)) |
36 | | simprlr 799 |
. . . . . 6
⊢ ((𝜑 ∧ (((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅) ∧ 𝑤 ∈ 𝑠)) → 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅) |
37 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ (((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅) ∧ 𝑤 ∈ 𝑠)) → 𝑤 ∈ 𝑠) |
38 | | uneq1 3722 |
. . . . . . . 8
⊢ (𝑣 = 𝑢 → (𝑣 ∪ {𝑤}) = (𝑢 ∪ {𝑤})) |
39 | 38 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑣 = 𝑢 → (𝑓‘(𝑣 ∪ {𝑤})) = (𝑓‘(𝑢 ∪ {𝑤}))) |
40 | 39 | cbvmptv 4678 |
. . . . . 6
⊢ (𝑣 ∈ ((𝑠 ∖ {𝑤})(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})(𝑀 − 1)) ↦ (𝑓‘(𝑣 ∪ {𝑤}))) = (𝑢 ∈ ((𝑠 ∖ {𝑤})(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})(𝑀 − 1)) ↦ (𝑓‘(𝑢 ∪ {𝑤}))) |
41 | 27, 28, 29, 30, 32, 33, 1, 34, 35, 36, 37, 40 | ramub1lem2 15569 |
. . . . 5
⊢ ((𝜑 ∧ (((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅) ∧ 𝑤 ∈ 𝑠)) → ∃𝑐 ∈ 𝑅 ∃𝑧 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) ⊆ (◡𝑓 “ {𝑐}))) |
42 | 41 | expr 641 |
. . . 4
⊢ ((𝜑 ∧ ((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅)) → (𝑤 ∈ 𝑠 → ∃𝑐 ∈ 𝑅 ∃𝑧 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
43 | 42 | exlimdv 1848 |
. . 3
⊢ ((𝜑 ∧ ((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅)) → (∃𝑤 𝑤 ∈ 𝑠 → ∃𝑐 ∈ 𝑅 ∃𝑧 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
44 | 26, 43 | mpd 15 |
. 2
⊢ ((𝜑 ∧ ((#‘𝑠) = (((𝑀 − 1) Ramsey 𝐺) + 1) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀)⟶𝑅)) → ∃𝑐 ∈ 𝑅 ∃𝑧 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})𝑀) ⊆ (◡𝑓 “ {𝑐}))) |
45 | 1, 3, 4, 8, 11, 44 | ramub2 15556 |
1
⊢ (𝜑 → (𝑀 Ramsey 𝐹) ≤ (((𝑀 − 1) Ramsey 𝐺) + 1)) |