Step | Hyp | Ref
| Expression |
1 | | df-ram 15705 |
. . 3
⊢ Ramsey =
(𝑚 ∈
ℕ0, 𝑟
∈ V ↦ inf({𝑛
∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))}, ℝ*, <
)) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → Ramsey =
(𝑚 ∈
ℕ0, 𝑟
∈ V ↦ inf({𝑛
∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))}, ℝ*, <
))) |
3 | | simplrr 801 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → 𝑟 = 𝐹) |
4 | 3 | dmeqd 5326 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → dom 𝑟 = dom 𝐹) |
5 | | simpll3 1102 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → 𝐹:𝑅⟶ℕ0) |
6 | | fdm 6051 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑅⟶ℕ0 → dom 𝐹 = 𝑅) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → dom 𝐹 = 𝑅) |
8 | 4, 7 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → dom 𝑟 = 𝑅) |
9 | | simplrl 800 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → 𝑚 = 𝑀) |
10 | 9 | eqeq2d 2632 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) →
((#‘𝑦) = 𝑚 ↔ (#‘𝑦) = 𝑀)) |
11 | 10 | rabbidv 3189 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚} = {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑀}) |
12 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑠 ∈ V |
13 | | simpll1 1100 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → 𝑀 ∈
ℕ0) |
14 | | ramval.c |
. . . . . . . . . . . . 13
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖}) |
15 | 14 | hashbcval 15706 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∈ V ∧ 𝑀 ∈ ℕ0)
→ (𝑠𝐶𝑀) = {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑀}) |
16 | 12, 13, 15 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → (𝑠𝐶𝑀) = {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑀}) |
17 | 11, 16 | eqtr4d 2659 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚} = (𝑠𝐶𝑀)) |
18 | 8, 17 | oveq12d 6668 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → (dom
𝑟
↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚}) = (𝑅 ↑𝑚 (𝑠𝐶𝑀))) |
19 | 18 | raleqdv 3144 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) →
(∀𝑓 ∈ (dom
𝑟
↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ∀𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))) |
20 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((𝑚 = 𝑀 ∧ 𝑟 = 𝐹) → 𝑟 = 𝐹) |
21 | 20 | dmeqd 5326 |
. . . . . . . . . . . 12
⊢ ((𝑚 = 𝑀 ∧ 𝑟 = 𝐹) → dom 𝑟 = dom 𝐹) |
22 | 6 | 3ad2ant3 1084 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → dom
𝐹 = 𝑅) |
23 | 21, 22 | sylan9eqr 2678 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) → dom 𝑟 = 𝑅) |
24 | 23 | ad2antrr 762 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) → dom 𝑟 = 𝑅) |
25 | 3 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → 𝑟 = 𝐹) |
26 | 25 | fveq1d 6193 |
. . . . . . . . . . . . 13
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑟‘𝑐) = (𝐹‘𝑐)) |
27 | 26 | breq1d 4663 |
. . . . . . . . . . . 12
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → ((𝑟‘𝑐) ≤ (#‘𝑥) ↔ (𝐹‘𝑐) ≤ (#‘𝑥))) |
28 | 9 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → 𝑚 = 𝑀) |
29 | 28 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥𝐶𝑚) = (𝑥𝐶𝑀)) |
30 | | vex 3203 |
. . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V |
31 | 13 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → 𝑀 ∈
ℕ0) |
32 | 28, 31 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → 𝑚 ∈ ℕ0) |
33 | 14 | hashbcval 15706 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ V ∧ 𝑚 ∈ ℕ0)
→ (𝑥𝐶𝑚) = {𝑦 ∈ 𝒫 𝑥 ∣ (#‘𝑦) = 𝑚}) |
34 | 30, 32, 33 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥𝐶𝑚) = {𝑦 ∈ 𝒫 𝑥 ∣ (#‘𝑦) = 𝑚}) |
35 | 29, 34 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥𝐶𝑀) = {𝑦 ∈ 𝒫 𝑥 ∣ (#‘𝑦) = 𝑚}) |
36 | 35 | sseq1d 3632 |
. . . . . . . . . . . . 13
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → ((𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}) ↔ {𝑦 ∈ 𝒫 𝑥 ∣ (#‘𝑦) = 𝑚} ⊆ (◡𝑓 “ {𝑐}))) |
37 | | rabss 3679 |
. . . . . . . . . . . . . 14
⊢ ({𝑦 ∈ 𝒫 𝑥 ∣ (#‘𝑦) = 𝑚} ⊆ (◡𝑓 “ {𝑐}) ↔ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → 𝑦 ∈ (◡𝑓 “ {𝑐}))) |
38 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀)) → 𝑓:(𝑠𝐶𝑀)⟶𝑅) |
39 | 38 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 𝑥 ∧ (#‘𝑦) = 𝑚)) → 𝑓:(𝑠𝐶𝑀)⟶𝑅) |
40 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓:(𝑠𝐶𝑀)⟶𝑅 → 𝑓 Fn (𝑠𝐶𝑀)) |
41 | | fniniseg 6338 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 Fn (𝑠𝐶𝑀) → (𝑦 ∈ (◡𝑓 “ {𝑐}) ↔ (𝑦 ∈ (𝑠𝐶𝑀) ∧ (𝑓‘𝑦) = 𝑐))) |
42 | 39, 40, 41 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 𝑥 ∧ (#‘𝑦) = 𝑚)) → (𝑦 ∈ (◡𝑓 “ {𝑐}) ↔ (𝑦 ∈ (𝑠𝐶𝑀) ∧ (𝑓‘𝑦) = 𝑐))) |
43 | 35 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑦 ∈ (𝑥𝐶𝑀) ↔ 𝑦 ∈ {𝑦 ∈ 𝒫 𝑥 ∣ (#‘𝑦) = 𝑚})) |
44 | | rabid 3116 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ {𝑦 ∈ 𝒫 𝑥 ∣ (#‘𝑦) = 𝑚} ↔ (𝑦 ∈ 𝒫 𝑥 ∧ (#‘𝑦) = 𝑚)) |
45 | 43, 44 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑦 ∈ (𝑥𝐶𝑀) ↔ (𝑦 ∈ 𝒫 𝑥 ∧ (#‘𝑦) = 𝑚))) |
46 | 45 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 𝑥 ∧ (#‘𝑦) = 𝑚)) → 𝑦 ∈ (𝑥𝐶𝑀)) |
47 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → 𝑠 ∈ V) |
48 | | elpwi 4168 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ 𝒫 𝑠 → 𝑥 ⊆ 𝑠) |
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → 𝑥 ⊆ 𝑠) |
50 | 14 | hashbcss 15708 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑠 ∈ V ∧ 𝑥 ⊆ 𝑠 ∧ 𝑀 ∈ ℕ0) → (𝑥𝐶𝑀) ⊆ (𝑠𝐶𝑀)) |
51 | 47, 49, 31, 50 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥𝐶𝑀) ⊆ (𝑠𝐶𝑀)) |
52 | 51 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ 𝑦 ∈ (𝑥𝐶𝑀)) → 𝑦 ∈ (𝑠𝐶𝑀)) |
53 | 46, 52 | syldan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 𝑥 ∧ (#‘𝑦) = 𝑚)) → 𝑦 ∈ (𝑠𝐶𝑀)) |
54 | 53 | biantrurd 529 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 𝑥 ∧ (#‘𝑦) = 𝑚)) → ((𝑓‘𝑦) = 𝑐 ↔ (𝑦 ∈ (𝑠𝐶𝑀) ∧ (𝑓‘𝑦) = 𝑐))) |
55 | 42, 54 | bitr4d 271 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 𝑥 ∧ (#‘𝑦) = 𝑚)) → (𝑦 ∈ (◡𝑓 “ {𝑐}) ↔ (𝑓‘𝑦) = 𝑐)) |
56 | 55 | anassrs 680 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ 𝑦 ∈ 𝒫 𝑥) ∧ (#‘𝑦) = 𝑚) → (𝑦 ∈ (◡𝑓 “ {𝑐}) ↔ (𝑓‘𝑦) = 𝑐)) |
57 | 56 | pm5.74da 723 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ 𝑦 ∈ 𝒫 𝑥) → (((#‘𝑦) = 𝑚 → 𝑦 ∈ (◡𝑓 “ {𝑐})) ↔ ((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐))) |
58 | 57 | ralbidva 2985 |
. . . . . . . . . . . . . 14
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → 𝑦 ∈ (◡𝑓 “ {𝑐})) ↔ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐))) |
59 | 37, 58 | syl5bb 272 |
. . . . . . . . . . . . 13
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → ({𝑦 ∈ 𝒫 𝑥 ∣ (#‘𝑦) = 𝑚} ⊆ (◡𝑓 “ {𝑐}) ↔ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐))) |
60 | 36, 59 | bitr2d 269 |
. . . . . . . . . . . 12
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐) ↔ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}))) |
61 | 27, 60 | anbi12d 747 |
. . . . . . . . . . 11
⊢
((((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
62 | 61 | rexbidva 3049 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) → (∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
63 | 24, 62 | rexeqbidv 3153 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))) → (∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
64 | 63 | ralbidva 2985 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) →
(∀𝑓 ∈ (𝑅 ↑𝑚
(𝑠𝐶𝑀))∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ∀𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
65 | 19, 64 | bitrd 268 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) →
(∀𝑓 ∈ (dom
𝑟
↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ∀𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))) |
66 | 65 | imbi2d 330 |
. . . . . 6
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → ((𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐))) ↔ (𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}))))) |
67 | 66 | albidv 1849 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) →
(∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐))) ↔ ∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}))))) |
68 | 67 | rabbidva 3188 |
. . . 4
⊢ (((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) → {𝑛 ∈ ℕ0 ∣
∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))} = {𝑛 ∈ ℕ0 ∣
∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))}) |
69 | | ramval.t |
. . . 4
⊢ 𝑇 = {𝑛 ∈ ℕ0 ∣
∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (𝑅 ↑𝑚 (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))} |
70 | 68, 69 | syl6eqr 2674 |
. . 3
⊢ (((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) → {𝑛 ∈ ℕ0 ∣
∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))} = 𝑇) |
71 | 70 | infeq1d 8383 |
. 2
⊢ (((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) → inf({𝑛 ∈ ℕ0 ∣
∀𝑠(𝑛 ≤ (#‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (#‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (#‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((#‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))}, ℝ*, < ) = inf(𝑇, ℝ*, <
)) |
72 | | simp1 1061 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → 𝑀 ∈
ℕ0) |
73 | | simp3 1063 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → 𝐹:𝑅⟶ℕ0) |
74 | | simp2 1062 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → 𝑅 ∈ 𝑉) |
75 | | fex 6490 |
. . 3
⊢ ((𝐹:𝑅⟶ℕ0 ∧ 𝑅 ∈ 𝑉) → 𝐹 ∈ V) |
76 | 73, 74, 75 | syl2anc 693 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → 𝐹 ∈ V) |
77 | | xrltso 11974 |
. . . 4
⊢ < Or
ℝ* |
78 | 77 | infex 8399 |
. . 3
⊢ inf(𝑇, ℝ*, < )
∈ V |
79 | 78 | a1i 11 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) →
inf(𝑇, ℝ*,
< ) ∈ V) |
80 | 2, 71, 72, 76, 79 | ovmpt2d 6788 |
1
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → (𝑀 Ramsey 𝐹) = inf(𝑇, ℝ*, <
)) |