Step | Hyp | Ref
| Expression |
1 | | rami.c |
. 2
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖}) |
2 | | rami.m |
. 2
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
3 | | rami.r |
. 2
⊢ (𝜑 → 𝑅 ∈ 𝑉) |
4 | | rami.f |
. 2
⊢ (𝜑 → 𝐹:𝑅⟶ℕ0) |
5 | | ramub2.n |
. 2
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
6 | 5 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) → 𝑁 ∈
ℕ0) |
7 | | hashfz1 13134 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (#‘(1...𝑁)) =
𝑁) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) → (#‘(1...𝑁)) = 𝑁) |
9 | | simprl 794 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) → 𝑁 ≤ (#‘𝑡)) |
10 | 8, 9 | eqbrtrd 4675 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) → (#‘(1...𝑁)) ≤ (#‘𝑡)) |
11 | | fzfid 12772 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) → (1...𝑁) ∈ Fin) |
12 | | vex 3203 |
. . . . . 6
⊢ 𝑡 ∈ V |
13 | | hashdom 13168 |
. . . . . 6
⊢
(((1...𝑁) ∈ Fin
∧ 𝑡 ∈ V) →
((#‘(1...𝑁)) ≤
(#‘𝑡) ↔
(1...𝑁) ≼ 𝑡)) |
14 | 11, 12, 13 | sylancl 694 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) → ((#‘(1...𝑁)) ≤ (#‘𝑡) ↔ (1...𝑁) ≼ 𝑡)) |
15 | 10, 14 | mpbid 222 |
. . . 4
⊢ ((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) → (1...𝑁) ≼ 𝑡) |
16 | 12 | domen 7968 |
. . . 4
⊢
((1...𝑁) ≼
𝑡 ↔ ∃𝑠((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) |
17 | 15, 16 | sylib 208 |
. . 3
⊢ ((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) → ∃𝑠((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) |
18 | | simpll 790 |
. . . . 5
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → 𝜑) |
19 | | ensym 8005 |
. . . . . . . 8
⊢
((1...𝑁) ≈
𝑠 → 𝑠 ≈ (1...𝑁)) |
20 | 19 | ad2antrl 764 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → 𝑠 ≈ (1...𝑁)) |
21 | | hasheni 13136 |
. . . . . . 7
⊢ (𝑠 ≈ (1...𝑁) → (#‘𝑠) = (#‘(1...𝑁))) |
22 | 20, 21 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → (#‘𝑠) = (#‘(1...𝑁))) |
23 | 5 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → 𝑁 ∈
ℕ0) |
24 | 23, 7 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → (#‘(1...𝑁)) = 𝑁) |
25 | 22, 24 | eqtrd 2656 |
. . . . 5
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → (#‘𝑠) = 𝑁) |
26 | | simplrr 801 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → 𝑔:(𝑡𝐶𝑀)⟶𝑅) |
27 | 12 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → 𝑡 ∈ V) |
28 | | simprr 796 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → 𝑠 ⊆ 𝑡) |
29 | 2 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → 𝑀 ∈
ℕ0) |
30 | 1 | hashbcss 15708 |
. . . . . . 7
⊢ ((𝑡 ∈ V ∧ 𝑠 ⊆ 𝑡 ∧ 𝑀 ∈ ℕ0) → (𝑠𝐶𝑀) ⊆ (𝑡𝐶𝑀)) |
31 | 27, 28, 29, 30 | syl3anc 1326 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → (𝑠𝐶𝑀) ⊆ (𝑡𝐶𝑀)) |
32 | 26, 31 | fssresd 6071 |
. . . . 5
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → (𝑔 ↾ (𝑠𝐶𝑀)):(𝑠𝐶𝑀)⟶𝑅) |
33 | | vex 3203 |
. . . . . . 7
⊢ 𝑔 ∈ V |
34 | 33 | resex 5443 |
. . . . . 6
⊢ (𝑔 ↾ (𝑠𝐶𝑀)) ∈ V |
35 | | feq1 6026 |
. . . . . . . . 9
⊢ (𝑓 = (𝑔 ↾ (𝑠𝐶𝑀)) → (𝑓:(𝑠𝐶𝑀)⟶𝑅 ↔ (𝑔 ↾ (𝑠𝐶𝑀)):(𝑠𝐶𝑀)⟶𝑅)) |
36 | 35 | anbi2d 740 |
. . . . . . . 8
⊢ (𝑓 = (𝑔 ↾ (𝑠𝐶𝑀)) → (((#‘𝑠) = 𝑁 ∧ 𝑓:(𝑠𝐶𝑀)⟶𝑅) ↔ ((#‘𝑠) = 𝑁 ∧ (𝑔 ↾ (𝑠𝐶𝑀)):(𝑠𝐶𝑀)⟶𝑅))) |
37 | 36 | anbi2d 740 |
. . . . . . 7
⊢ (𝑓 = (𝑔 ↾ (𝑠𝐶𝑀)) → ((𝜑 ∧ ((#‘𝑠) = 𝑁 ∧ 𝑓:(𝑠𝐶𝑀)⟶𝑅)) ↔ (𝜑 ∧ ((#‘𝑠) = 𝑁 ∧ (𝑔 ↾ (𝑠𝐶𝑀)):(𝑠𝐶𝑀)⟶𝑅)))) |
38 | | cnveq 5296 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑔 ↾ (𝑠𝐶𝑀)) → ◡𝑓 = ◡(𝑔 ↾ (𝑠𝐶𝑀))) |
39 | 38 | imaeq1d 5465 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑔 ↾ (𝑠𝐶𝑀)) → (◡𝑓 “ {𝑐}) = (◡(𝑔 ↾ (𝑠𝐶𝑀)) “ {𝑐})) |
40 | | cnvresima 5623 |
. . . . . . . . . . 11
⊢ (◡(𝑔 ↾ (𝑠𝐶𝑀)) “ {𝑐}) = ((◡𝑔 “ {𝑐}) ∩ (𝑠𝐶𝑀)) |
41 | 39, 40 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑔 ↾ (𝑠𝐶𝑀)) → (◡𝑓 “ {𝑐}) = ((◡𝑔 “ {𝑐}) ∩ (𝑠𝐶𝑀))) |
42 | 41 | sseq2d 3633 |
. . . . . . . . 9
⊢ (𝑓 = (𝑔 ↾ (𝑠𝐶𝑀)) → ((𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}) ↔ (𝑥𝐶𝑀) ⊆ ((◡𝑔 “ {𝑐}) ∩ (𝑠𝐶𝑀)))) |
43 | 42 | anbi2d 740 |
. . . . . . . 8
⊢ (𝑓 = (𝑔 ↾ (𝑠𝐶𝑀)) → (((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})) ↔ ((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ ((◡𝑔 “ {𝑐}) ∩ (𝑠𝐶𝑀))))) |
44 | 43 | 2rexbidv 3057 |
. . . . . . 7
⊢ (𝑓 = (𝑔 ↾ (𝑠𝐶𝑀)) → (∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})) ↔ ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ ((◡𝑔 “ {𝑐}) ∩ (𝑠𝐶𝑀))))) |
45 | 37, 44 | imbi12d 334 |
. . . . . 6
⊢ (𝑓 = (𝑔 ↾ (𝑠𝐶𝑀)) → (((𝜑 ∧ ((#‘𝑠) = 𝑁 ∧ 𝑓:(𝑠𝐶𝑀)⟶𝑅)) → ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}))) ↔ ((𝜑 ∧ ((#‘𝑠) = 𝑁 ∧ (𝑔 ↾ (𝑠𝐶𝑀)):(𝑠𝐶𝑀)⟶𝑅)) → ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ ((◡𝑔 “ {𝑐}) ∩ (𝑠𝐶𝑀)))))) |
46 | | ramub2.i |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘𝑠) = 𝑁 ∧ 𝑓:(𝑠𝐶𝑀)⟶𝑅)) → ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}))) |
47 | 34, 45, 46 | vtocl 3259 |
. . . . 5
⊢ ((𝜑 ∧ ((#‘𝑠) = 𝑁 ∧ (𝑔 ↾ (𝑠𝐶𝑀)):(𝑠𝐶𝑀)⟶𝑅)) → ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ ((◡𝑔 “ {𝑐}) ∩ (𝑠𝐶𝑀)))) |
48 | 18, 25, 32, 47 | syl12anc 1324 |
. . . 4
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ ((◡𝑔 “ {𝑐}) ∩ (𝑠𝐶𝑀)))) |
49 | | sstr 3611 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑡) → 𝑥 ⊆ 𝑡) |
50 | 49 | expcom 451 |
. . . . . . . . 9
⊢ (𝑠 ⊆ 𝑡 → (𝑥 ⊆ 𝑠 → 𝑥 ⊆ 𝑡)) |
51 | 50 | ad2antll 765 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → (𝑥 ⊆ 𝑠 → 𝑥 ⊆ 𝑡)) |
52 | | selpw 4165 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 𝑠 ↔ 𝑥 ⊆ 𝑠) |
53 | | selpw 4165 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 𝑡 ↔ 𝑥 ⊆ 𝑡) |
54 | 51, 52, 53 | 3imtr4g 285 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → (𝑥 ∈ 𝒫 𝑠 → 𝑥 ∈ 𝒫 𝑡)) |
55 | | id 22 |
. . . . . . . . . 10
⊢ ((𝑥𝐶𝑀) ⊆ ((◡𝑔 “ {𝑐}) ∩ (𝑠𝐶𝑀)) → (𝑥𝐶𝑀) ⊆ ((◡𝑔 “ {𝑐}) ∩ (𝑠𝐶𝑀))) |
56 | | inss1 3833 |
. . . . . . . . . 10
⊢ ((◡𝑔 “ {𝑐}) ∩ (𝑠𝐶𝑀)) ⊆ (◡𝑔 “ {𝑐}) |
57 | 55, 56 | syl6ss 3615 |
. . . . . . . . 9
⊢ ((𝑥𝐶𝑀) ⊆ ((◡𝑔 “ {𝑐}) ∩ (𝑠𝐶𝑀)) → (𝑥𝐶𝑀) ⊆ (◡𝑔 “ {𝑐})) |
58 | 57 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → ((𝑥𝐶𝑀) ⊆ ((◡𝑔 “ {𝑐}) ∩ (𝑠𝐶𝑀)) → (𝑥𝐶𝑀) ⊆ (◡𝑔 “ {𝑐}))) |
59 | 58 | anim2d 589 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → (((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ ((◡𝑔 “ {𝑐}) ∩ (𝑠𝐶𝑀))) → ((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑔 “ {𝑐})))) |
60 | 54, 59 | anim12d 586 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → ((𝑥 ∈ 𝒫 𝑠 ∧ ((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ ((◡𝑔 “ {𝑐}) ∩ (𝑠𝐶𝑀)))) → (𝑥 ∈ 𝒫 𝑡 ∧ ((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑔 “ {𝑐}))))) |
61 | 60 | reximdv2 3014 |
. . . . 5
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → (∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ ((◡𝑔 “ {𝑐}) ∩ (𝑠𝐶𝑀))) → ∃𝑥 ∈ 𝒫 𝑡((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑔 “ {𝑐})))) |
62 | 61 | reximdv 3016 |
. . . 4
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → (∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ ((◡𝑔 “ {𝑐}) ∩ (𝑠𝐶𝑀))) → ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑡((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑔 “ {𝑐})))) |
63 | 48, 62 | mpd 15 |
. . 3
⊢ (((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) ∧ ((1...𝑁) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡)) → ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑡((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑔 “ {𝑐}))) |
64 | 17, 63 | exlimddv 1863 |
. 2
⊢ ((𝜑 ∧ (𝑁 ≤ (#‘𝑡) ∧ 𝑔:(𝑡𝐶𝑀)⟶𝑅)) → ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑡((𝐹‘𝑐) ≤ (#‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑔 “ {𝑐}))) |
65 | 1, 2, 3, 4, 5, 64 | ramub 15717 |
1
⊢ (𝜑 → (𝑀 Ramsey 𝐹) ≤ 𝑁) |