Step | Hyp | Ref
| Expression |
1 | | df-ram 15543 |
. . 3
⊢ Ramsey =
(𝑚 ∈
ℕ0, 𝑟
∈ V ↦ inf({𝑛
∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))}, ℝ*, <
)) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → Ramsey =
(𝑚 ∈
ℕ0, 𝑟
∈ V ↦ inf({𝑛
∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))}, ℝ*, <
))) |
3 | | simplrr 797 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → 𝑟 = 𝐹) |
4 | 3 | dmeqd 5248 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → dom 𝑟 = dom 𝐹) |
5 | | simpll3 1095 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → 𝐹:𝑅⟶ℕ0) |
6 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑅⟶ℕ0 → dom 𝐹 = 𝑅) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → dom 𝐹 = 𝑅) |
8 | 4, 7 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → dom 𝑟 = 𝑅) |
9 | | simplrl 796 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → 𝑚 = 𝑀) |
10 | 9 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) →
((#‘𝑦) = 𝑚 ↔ (#‘𝑦) = 𝑀)) |
11 | 10 | rabbidv 3164 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚} = {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑀}) |
12 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑠 ∈ V |
13 | | simpll1 1093 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → 𝑀 ∈
ℕ0) |
14 | | ramval.c |
. . . . . . . . . . . . 13
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖}) |
15 | 14 | hashbcval 15544 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∈ V ∧ 𝑀 ∈ ℕ0)
→ (𝑠𝐶𝑀) = {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑀}) |
16 | 12, 13, 15 | sylancr 694 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → (𝑠𝐶𝑀) = {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑀}) |
17 | 11, 16 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚} = (𝑠𝐶𝑀)) |
18 | 8, 17 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → (dom
𝑟
↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚}) = (𝑅 ↑𝑚 (𝑠𝐶𝑀))) |
19 | 18 | raleqdv 3121 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) →
(∀𝑓 ∈ (dom
𝑟
↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ∀𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))) |
20 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝑚 = 𝑀 ∧ 𝑟 = 𝐹) → 𝑟 = 𝐹) |
21 | 20 | dmeqd 5248 |
. . . . . . . . . . . 12
⊢ ((𝑚 = 𝑀 ∧ 𝑟 = 𝐹) → dom 𝑟 = dom 𝐹) |
22 | 6 | 3ad2ant3 1077 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → dom
𝐹 = 𝑅) |
23 | 21, 22 | sylan9eqr 2666 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) → dom 𝑟 = 𝑅) |
24 | 23 | ad2antrr 758 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) → dom 𝑟 = 𝑅) |
25 | 3 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → 𝑟 = 𝐹) |
26 | 25 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑟‘𝑐) = (𝐹‘𝑐)) |
27 | 26 | breq1d 4593 |
. . . . . . . . . . . 12
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → ((𝑟‘𝑐) ≤ (#‘𝑥) ↔ (𝐹‘𝑐) ≤ (#‘𝑥))) |
28 | 9 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → 𝑚 = 𝑀) |
29 | 28 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥𝐶𝑚) = (𝑥𝐶𝑀)) |
30 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V |
31 | 13 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → 𝑀 ∈
ℕ0) |
32 | 28, 31 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → 𝑚 ∈ ℕ0) |
33 | 14 | hashbcval 15544 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ V ∧ 𝑚 ∈ ℕ0)
→ (𝑥𝐶𝑚) = {𝑦 ∈ 𝒫 𝑥 ∣ (#‘𝑦) = 𝑚}) |
34 | 30, 32, 33 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥𝐶𝑚) = {𝑦 ∈ 𝒫 𝑥 ∣ (#‘𝑦) = 𝑚}) |
35 | 29, 34 | eqtr3d 2646 |
. . . . . . . . . . . . . 14
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥𝐶𝑀) = {𝑦 ∈ 𝒫 𝑥 ∣ (#‘𝑦) = 𝑚}) |
36 | 35 | sseq1d 3595 |
. . . . . . . . . . . . 13
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → ((𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}) ↔ {𝑦 ∈ 𝒫 𝑥 ∣ (#‘𝑦) = 𝑚} ⊆ (◡𝑓 “ {𝑐}))) |
37 | | rabss 3642 |
. . . . . . . . . . . . . 14
⊢ ({𝑦 ∈ 𝒫 𝑥 ∣ (#‘𝑦) = 𝑚} ⊆ (◡𝑓 “ {𝑐}) ↔ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → 𝑦 ∈ (◡𝑓 “ {𝑐}))) |
38 | | elmapi 7765 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀)) → 𝑓:(𝑠𝐶𝑀)⟶𝑅) |
39 | 38 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 𝑥 ∧ (#‘𝑦) = 𝑚)) → 𝑓:(𝑠𝐶𝑀)⟶𝑅) |
40 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓:(𝑠𝐶𝑀)⟶𝑅 → 𝑓 Fn (𝑠𝐶𝑀)) |
41 | | fniniseg 6246 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 Fn (𝑠𝐶𝑀) → (𝑦 ∈ (◡𝑓 “ {𝑐}) ↔ (𝑦 ∈ (𝑠𝐶𝑀) ∧ (𝑓‘𝑦) = 𝑐))) |
42 | 39, 40, 41 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 𝑥 ∧ (#‘𝑦) = 𝑚)) → (𝑦 ∈ (◡𝑓 “ {𝑐}) ↔ (𝑦 ∈ (𝑠𝐶𝑀) ∧ (𝑓‘𝑦) = 𝑐))) |
43 | 35 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑦 ∈ (𝑥𝐶𝑀) ↔ 𝑦 ∈ {𝑦 ∈ 𝒫 𝑥 ∣ (#‘𝑦) = 𝑚})) |
44 | | rabid 3095 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ {𝑦 ∈ 𝒫 𝑥 ∣ (#‘𝑦) = 𝑚} ↔ (𝑦 ∈ 𝒫 𝑥 ∧ (#‘𝑦) = 𝑚)) |
45 | 43, 44 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑦 ∈ (𝑥𝐶𝑀) ↔ (𝑦 ∈ 𝒫 𝑥 ∧ (#‘𝑦) = 𝑚))) |
46 | 45 | biimpar 501 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 𝑥 ∧ (#‘𝑦) = 𝑚)) → 𝑦 ∈ (𝑥𝐶𝑀)) |
47 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → 𝑠 ∈ V) |
48 | | elpwi 4117 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ 𝒫 𝑠 → 𝑥 ⊆ 𝑠) |
49 | 48 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → 𝑥 ⊆ 𝑠) |
50 | 14 | hashbcss 15546 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑠 ∈ V ∧ 𝑥 ⊆ 𝑠 ∧ 𝑀 ∈ ℕ0) → (𝑥𝐶𝑀) ⊆ (𝑠𝐶𝑀)) |
51 | 47, 49, 31, 50 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥𝐶𝑀) ⊆ (𝑠𝐶𝑀)) |
52 | 51 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ 𝑦 ∈ (𝑥𝐶𝑀)) → 𝑦 ∈ (𝑠𝐶𝑀)) |
53 | 46, 52 | syldan 486 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 𝑥 ∧ (#‘𝑦) = 𝑚)) → 𝑦 ∈ (𝑠𝐶𝑀)) |
54 | 53 | biantrurd 528 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 𝑥 ∧ (#‘𝑦) = 𝑚)) → ((𝑓‘𝑦) = 𝑐 ↔ (𝑦 ∈ (𝑠𝐶𝑀) ∧ (𝑓‘𝑦) = 𝑐))) |
55 | 42, 54 | bitr4d 270 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 𝑥 ∧ (#‘𝑦) = 𝑚)) → (𝑦 ∈ (◡𝑓 “ {𝑐}) ↔ (𝑓‘𝑦) = 𝑐)) |
56 | 55 | anassrs 678 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ 𝑦 ∈ 𝒫 𝑥) ∧ (#‘𝑦) = 𝑚) → (𝑦 ∈ (◡𝑓 “ {𝑐}) ↔ (𝑓‘𝑦) = 𝑐)) |
57 | 56 | pm5.74da 719 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ 𝑦 ∈ 𝒫 𝑥) → (((#‘𝑦) = 𝑚 → 𝑦 ∈ (◡𝑓 “ {𝑐})) ↔ ((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐))) |
58 | 57 | ralbidva 2968 |
. . . . . . . . . . . . . 14
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → 𝑦 ∈ (◡𝑓 “ {𝑐})) ↔ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐))) |
59 | 37, 58 | syl5bb 271 |
. . . . . . . . . . . . 13
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → ({𝑦 ∈ 𝒫 𝑥 ∣ (#‘𝑦) = 𝑚} ⊆ (◡𝑓 “ {𝑐}) ↔ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐))) |
60 | 36, 59 | bitr2d 268 |
. . . . . . . . . . . 12
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐) ↔ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}))) |
61 | 27, 60 | anbi12d 743 |
. . . . . . . . . . 11
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
62 | 61 | rexbidva 3031 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) → (∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
63 | 24, 62 | rexeqbidv 3130 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) → (∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
64 | 63 | ralbidva 2968 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) →
(∀𝑓 ∈ (𝑅 ↑𝑚
(𝑠𝐶𝑀))∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ∀𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
65 | 19, 64 | bitrd 267 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) →
(∀𝑓 ∈ (dom
𝑟
↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ∀𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
66 | 65 | imbi2d 329 |
. . . . . 6
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → ((𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐))) ↔ (𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}))))) |
67 | 66 | albidv 1836 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) →
(∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐))) ↔ ∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}))))) |
68 | 67 | rabbidva 3163 |
. . . 4
⊢ (((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) → {𝑛 ∈ ℕ0 ∣
∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))} = {𝑛 ∈ ℕ0 ∣
∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))}) |
69 | | ramval.t |
. . . 4
⊢ 𝑇 = {𝑛 ∈ ℕ0 ∣
∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))} |
70 | 68, 69 | syl6eqr 2662 |
. . 3
⊢ (((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) → {𝑛 ∈ ℕ0 ∣
∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))} = 𝑇) |
71 | 70 | infeq1d 8266 |
. 2
⊢ (((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) → inf({𝑛 ∈ ℕ0 ∣
∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))}, ℝ*, < ) = inf(𝑇, ℝ*, <
)) |
72 | | simp1 1054 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → 𝑀 ∈
ℕ0) |
73 | | simp3 1056 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → 𝐹:𝑅⟶ℕ0) |
74 | | simp2 1055 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → 𝑅 ∈ 𝑉) |
75 | | fex 6394 |
. . 3
⊢ ((𝐹:𝑅⟶ℕ0 ∧ 𝑅 ∈ 𝑉) → 𝐹 ∈ V) |
76 | 73, 74, 75 | syl2anc 691 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → 𝐹 ∈ V) |
77 | | xrltso 11850 |
. . . 4
⊢ < Or
ℝ* |
78 | 77 | infex 8282 |
. . 3
⊢ inf(𝑇, ℝ*, < )
∈ V |
79 | 78 | a1i 11 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) →
inf(𝑇, ℝ*,
< ) ∈ V) |
80 | 2, 71, 72, 76, 79 | ovmpt2d 6686 |
1
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → (𝑀 Ramsey 𝐹) = inf(𝑇, ℝ*, <
)) |