Step | Hyp | Ref
| Expression |
1 | | ramub1.3 |
. . 3
β’ πΆ = (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π}) |
2 | | ramub1.m |
. . . 4
β’ (π β π β β) |
3 | | nnm1nn0 12316 |
. . . 4
β’ (π β β β (π β 1) β
β0) |
4 | 2, 3 | syl 17 |
. . 3
β’ (π β (π β 1) β
β0) |
5 | | ramub1.r |
. . 3
β’ (π β π
β Fin) |
6 | | ramub1.1 |
. . 3
β’ (π β πΊ:π
βΆβ0) |
7 | | ramub1.2 |
. . 3
β’ (π β ((π β 1) Ramsey πΊ) β
β0) |
8 | | ramub1.4 |
. . . 4
β’ (π β π β Fin) |
9 | | diffi 8996 |
. . . 4
β’ (π β Fin β (π β {π}) β Fin) |
10 | 8, 9 | syl 17 |
. . 3
β’ (π β (π β {π}) β Fin) |
11 | 7 | nn0red 12336 |
. . . . 5
β’ (π β ((π β 1) Ramsey πΊ) β β) |
12 | 11 | leidd 11583 |
. . . 4
β’ (π β ((π β 1) Ramsey πΊ) β€ ((π β 1) Ramsey πΊ)) |
13 | | hashcl 14112 |
. . . . . . 7
β’ ((π β {π}) β Fin β (β―β(π β {π})) β
β0) |
14 | 10, 13 | syl 17 |
. . . . . 6
β’ (π β (β―β(π β {π})) β
β0) |
15 | 14 | nn0cnd 12337 |
. . . . 5
β’ (π β (β―β(π β {π})) β β) |
16 | 7 | nn0cnd 12337 |
. . . . 5
β’ (π β ((π β 1) Ramsey πΊ) β β) |
17 | | 1cnd 11012 |
. . . . 5
β’ (π β 1 β
β) |
18 | | undif1 4415 |
. . . . . . . 8
β’ ((π β {π}) βͺ {π}) = (π βͺ {π}) |
19 | | ramub1.x |
. . . . . . . . . 10
β’ (π β π β π) |
20 | 19 | snssd 4748 |
. . . . . . . . 9
β’ (π β {π} β π) |
21 | | ssequn2 4123 |
. . . . . . . . 9
β’ ({π} β π β (π βͺ {π}) = π) |
22 | 20, 21 | sylib 217 |
. . . . . . . 8
β’ (π β (π βͺ {π}) = π) |
23 | 18, 22 | eqtrid 2788 |
. . . . . . 7
β’ (π β ((π β {π}) βͺ {π}) = π) |
24 | 23 | fveq2d 6804 |
. . . . . 6
β’ (π β (β―β((π β {π}) βͺ {π})) = (β―βπ)) |
25 | | neldifsnd 4732 |
. . . . . . 7
β’ (π β Β¬ π β (π β {π})) |
26 | | hashunsng 14148 |
. . . . . . . 8
β’ (π β π β (((π β {π}) β Fin β§ Β¬ π β (π β {π})) β (β―β((π β {π}) βͺ {π})) = ((β―β(π β {π})) + 1))) |
27 | 19, 26 | syl 17 |
. . . . . . 7
β’ (π β (((π β {π}) β Fin β§ Β¬ π β (π β {π})) β (β―β((π β {π}) βͺ {π})) = ((β―β(π β {π})) + 1))) |
28 | 10, 25, 27 | mp2and 697 |
. . . . . 6
β’ (π β (β―β((π β {π}) βͺ {π})) = ((β―β(π β {π})) + 1)) |
29 | | ramub1.5 |
. . . . . 6
β’ (π β (β―βπ) = (((π β 1) Ramsey πΊ) + 1)) |
30 | 24, 28, 29 | 3eqtr3d 2784 |
. . . . 5
β’ (π β ((β―β(π β {π})) + 1) = (((π β 1) Ramsey πΊ) + 1)) |
31 | 15, 16, 17, 30 | addcan2ad 11223 |
. . . 4
β’ (π β (β―β(π β {π})) = ((π β 1) Ramsey πΊ)) |
32 | 12, 31 | breqtrrd 5109 |
. . 3
β’ (π β ((π β 1) Ramsey πΊ) β€ (β―β(π β {π}))) |
33 | | ramub1.6 |
. . . . . 6
β’ (π β πΎ:(ππΆπ)βΆπ
) |
34 | 33 | adantr 482 |
. . . . 5
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β πΎ:(ππΆπ)βΆπ
) |
35 | | fveqeq2 6809 |
. . . . . . 7
β’ (π₯ = (π’ βͺ {π}) β ((β―βπ₯) = π β (β―β(π’ βͺ {π})) = π)) |
36 | 1 | hashbcval 16744 |
. . . . . . . . . . . . . . 15
β’ (((π β {π}) β Fin β§ (π β 1) β β0)
β ((π β {π})πΆ(π β 1)) = {π₯ β π« (π β {π}) β£ (β―βπ₯) = (π β 1)}) |
37 | 10, 4, 36 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β ((π β {π})πΆ(π β 1)) = {π₯ β π« (π β {π}) β£ (β―βπ₯) = (π β 1)}) |
38 | 37 | eleq2d 2822 |
. . . . . . . . . . . . 13
β’ (π β (π’ β ((π β {π})πΆ(π β 1)) β π’ β {π₯ β π« (π β {π}) β£ (β―βπ₯) = (π β 1)})) |
39 | | fveqeq2 6809 |
. . . . . . . . . . . . . 14
β’ (π₯ = π’ β ((β―βπ₯) = (π β 1) β (β―βπ’) = (π β 1))) |
40 | 39 | elrab 3629 |
. . . . . . . . . . . . 13
β’ (π’ β {π₯ β π« (π β {π}) β£ (β―βπ₯) = (π β 1)} β (π’ β π« (π β {π}) β§ (β―βπ’) = (π β 1))) |
41 | 38, 40 | bitrdi 288 |
. . . . . . . . . . . 12
β’ (π β (π’ β ((π β {π})πΆ(π β 1)) β (π’ β π« (π β {π}) β§ (β―βπ’) = (π β 1)))) |
42 | 41 | simprbda 500 |
. . . . . . . . . . 11
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β π’ β π« (π β {π})) |
43 | 42 | elpwid 4548 |
. . . . . . . . . 10
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β π’ β (π β {π})) |
44 | 43 | difss2d 4075 |
. . . . . . . . 9
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β π’ β π) |
45 | 20 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β {π} β π) |
46 | 44, 45 | unssd 4126 |
. . . . . . . 8
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β (π’ βͺ {π}) β π) |
47 | | vex 3441 |
. . . . . . . . . 10
β’ π’ β V |
48 | | snex 5363 |
. . . . . . . . . 10
β’ {π} β V |
49 | 47, 48 | unex 7624 |
. . . . . . . . 9
β’ (π’ βͺ {π}) β V |
50 | 49 | elpw 4543 |
. . . . . . . 8
β’ ((π’ βͺ {π}) β π« π β (π’ βͺ {π}) β π) |
51 | 46, 50 | sylibr 234 |
. . . . . . 7
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β (π’ βͺ {π}) β π« π) |
52 | 10 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β (π β {π}) β Fin) |
53 | 52, 43 | ssfid 9082 |
. . . . . . . . 9
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β π’ β Fin) |
54 | | neldifsnd 4732 |
. . . . . . . . . 10
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β Β¬ π β (π β {π})) |
55 | 43, 54 | ssneldd 3929 |
. . . . . . . . 9
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β Β¬ π β π’) |
56 | 19 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β π β π) |
57 | | hashunsng 14148 |
. . . . . . . . . 10
β’ (π β π β ((π’ β Fin β§ Β¬ π β π’) β (β―β(π’ βͺ {π})) = ((β―βπ’) + 1))) |
58 | 56, 57 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β ((π’ β Fin β§ Β¬ π β π’) β (β―β(π’ βͺ {π})) = ((β―βπ’) + 1))) |
59 | 53, 55, 58 | mp2and 697 |
. . . . . . . 8
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β (β―β(π’ βͺ {π})) = ((β―βπ’) + 1)) |
60 | 41 | simplbda 501 |
. . . . . . . . 9
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β (β―βπ’) = (π β 1)) |
61 | 60 | oveq1d 7318 |
. . . . . . . 8
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β ((β―βπ’) + 1) = ((π β 1) + 1)) |
62 | 2 | nncnd 12031 |
. . . . . . . . . 10
β’ (π β π β β) |
63 | | ax-1cn 10971 |
. . . . . . . . . 10
β’ 1 β
β |
64 | | npcan 11272 |
. . . . . . . . . 10
β’ ((π β β β§ 1 β
β) β ((π β
1) + 1) = π) |
65 | 62, 63, 64 | sylancl 587 |
. . . . . . . . 9
β’ (π β ((π β 1) + 1) = π) |
66 | 65 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β ((π β 1) + 1) = π) |
67 | 59, 61, 66 | 3eqtrd 2780 |
. . . . . . 7
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β (β―β(π’ βͺ {π})) = π) |
68 | 35, 51, 67 | elrabd 3631 |
. . . . . 6
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β (π’ βͺ {π}) β {π₯ β π« π β£ (β―βπ₯) = π}) |
69 | 2 | nnnn0d 12335 |
. . . . . . . 8
β’ (π β π β
β0) |
70 | 1 | hashbcval 16744 |
. . . . . . . 8
β’ ((π β Fin β§ π β β0)
β (ππΆπ) = {π₯ β π« π β£ (β―βπ₯) = π}) |
71 | 8, 69, 70 | syl2anc 585 |
. . . . . . 7
β’ (π β (ππΆπ) = {π₯ β π« π β£ (β―βπ₯) = π}) |
72 | 71 | adantr 482 |
. . . . . 6
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β (ππΆπ) = {π₯ β π« π β£ (β―βπ₯) = π}) |
73 | 68, 72 | eleqtrrd 2840 |
. . . . 5
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β (π’ βͺ {π}) β (ππΆπ)) |
74 | 34, 73 | ffvelcdmd 6990 |
. . . 4
β’ ((π β§ π’ β ((π β {π})πΆ(π β 1))) β (πΎβ(π’ βͺ {π})) β π
) |
75 | | ramub1.h |
. . . 4
β’ π» = (π’ β ((π β {π})πΆ(π β 1)) β¦ (πΎβ(π’ βͺ {π}))) |
76 | 74, 75 | fmptd 7016 |
. . 3
β’ (π β π»:((π β {π})πΆ(π β 1))βΆπ
) |
77 | 1, 4, 5, 6, 7, 10,
32, 76 | rami 16757 |
. 2
β’ (π β βπ β π
βπ€ β π« (π β {π})((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π}))) |
78 | 69 | adantr 482 |
. . . . . 6
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β π β
β0) |
79 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β π
β Fin) |
80 | | ramub1.f |
. . . . . . . . . . . 12
β’ (π β πΉ:π
βΆβ) |
81 | 80 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β πΉ:π
βΆβ) |
82 | | simprll 777 |
. . . . . . . . . . 11
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β π β π
) |
83 | 81, 82 | ffvelcdmd 6990 |
. . . . . . . . . 10
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β (πΉβπ) β β) |
84 | | nnm1nn0 12316 |
. . . . . . . . . 10
β’ ((πΉβπ) β β β ((πΉβπ) β 1) β
β0) |
85 | 83, 84 | syl 17 |
. . . . . . . . 9
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β ((πΉβπ) β 1) β
β0) |
86 | 85 | adantr 482 |
. . . . . . . 8
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ π¦ β π
) β ((πΉβπ) β 1) β
β0) |
87 | 81 | ffvelcdmda 6989 |
. . . . . . . . 9
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ π¦ β π
) β (πΉβπ¦) β β) |
88 | 87 | nnnn0d 12335 |
. . . . . . . 8
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ π¦ β π
) β (πΉβπ¦) β
β0) |
89 | 86, 88 | ifcld 4511 |
. . . . . . 7
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ π¦ β π
) β if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦)) β
β0) |
90 | | eqid 2736 |
. . . . . . 7
β’ (π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦))) = (π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦))) |
91 | 89, 90 | fmptd 7016 |
. . . . . 6
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β (π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦))):π
βΆβ0) |
92 | | equequ2 2027 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π¦ = π₯ β π¦ = π)) |
93 | | fveq2 6800 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
94 | 93 | oveq1d 7318 |
. . . . . . . . . . . 12
β’ (π₯ = π β ((πΉβπ₯) β 1) = ((πΉβπ) β 1)) |
95 | 92, 94 | ifbieq1d 4489 |
. . . . . . . . . . 11
β’ (π₯ = π β if(π¦ = π₯, ((πΉβπ₯) β 1), (πΉβπ¦)) = if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦))) |
96 | 95 | mpteq2dv 5183 |
. . . . . . . . . 10
β’ (π₯ = π β (π¦ β π
β¦ if(π¦ = π₯, ((πΉβπ₯) β 1), (πΉβπ¦))) = (π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦)))) |
97 | 96 | oveq2d 7319 |
. . . . . . . . 9
β’ (π₯ = π β (π Ramsey (π¦ β π
β¦ if(π¦ = π₯, ((πΉβπ₯) β 1), (πΉβπ¦)))) = (π Ramsey (π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦))))) |
98 | | ramub1.g |
. . . . . . . . 9
β’ πΊ = (π₯ β π
β¦ (π Ramsey (π¦ β π
β¦ if(π¦ = π₯, ((πΉβπ₯) β 1), (πΉβπ¦))))) |
99 | | ovex 7336 |
. . . . . . . . 9
β’ (π Ramsey (π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦)))) β V |
100 | 97, 98, 99 | fvmpt 6903 |
. . . . . . . 8
β’ (π β π
β (πΊβπ) = (π Ramsey (π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦))))) |
101 | 82, 100 | syl 17 |
. . . . . . 7
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β (πΊβπ) = (π Ramsey (π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦))))) |
102 | 6 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β πΊ:π
βΆβ0) |
103 | 102, 82 | ffvelcdmd 6990 |
. . . . . . 7
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β (πΊβπ) β
β0) |
104 | 101, 103 | eqeltrrd 2838 |
. . . . . 6
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β (π Ramsey (π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦)))) β
β0) |
105 | | simprlr 778 |
. . . . . 6
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β π€ β π« (π β {π})) |
106 | | simprrl 779 |
. . . . . . 7
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β (πΊβπ) β€ (β―βπ€)) |
107 | 101, 106 | eqbrtrrd 5105 |
. . . . . 6
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β (π Ramsey (π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦)))) β€ (β―βπ€)) |
108 | 33 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β πΎ:(ππΆπ)βΆπ
) |
109 | 8 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β π β Fin) |
110 | 105 | elpwid 4548 |
. . . . . . . . 9
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β π€ β (π β {π})) |
111 | 110 | difss2d 4075 |
. . . . . . . 8
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β π€ β π) |
112 | 1 | hashbcss 16746 |
. . . . . . . 8
β’ ((π β Fin β§ π€ β π β§ π β β0) β (π€πΆπ) β (ππΆπ)) |
113 | 109, 111,
78, 112 | syl3anc 1371 |
. . . . . . 7
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β (π€πΆπ) β (ππΆπ)) |
114 | 108, 113 | fssresd 6667 |
. . . . . 6
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β (πΎ βΎ (π€πΆπ)):(π€πΆπ)βΆπ
) |
115 | 1, 78, 79, 91, 104, 105, 107, 114 | rami 16757 |
. . . . 5
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β βπ β π
βπ£ β π« π€(((π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦)))βπ) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π}))) |
116 | | equequ1 2026 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β (π¦ = π β π = π)) |
117 | | fveq2 6800 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β (πΉβπ¦) = (πΉβπ)) |
118 | 116, 117 | ifbieq2d 4491 |
. . . . . . . . . . . . 13
β’ (π¦ = π β if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦)) = if(π = π, ((πΉβπ) β 1), (πΉβπ))) |
119 | | ovex 7336 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ) β 1) β V |
120 | | fvex 6813 |
. . . . . . . . . . . . . 14
β’ (πΉβπ) β V |
121 | 119, 120 | ifex 4515 |
. . . . . . . . . . . . 13
β’ if(π = π, ((πΉβπ) β 1), (πΉβπ)) β V |
122 | 118, 90, 121 | fvmpt 6903 |
. . . . . . . . . . . 12
β’ (π β π
β ((π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦)))βπ) = if(π = π, ((πΉβπ) β 1), (πΉβπ))) |
123 | 122 | ad2antrl 726 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ (π β π
β§ π£ β π« π€)) β ((π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦)))βπ) = if(π = π, ((πΉβπ) β 1), (πΉβπ))) |
124 | 123 | breq1d 5091 |
. . . . . . . . . 10
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ (π β π
β§ π£ β π« π€)) β (((π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦)))βπ) β€ (β―βπ£) β if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£))) |
125 | 124 | anbi1d 631 |
. . . . . . . . 9
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ (π β π
β§ π£ β π« π€)) β ((((π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦)))βπ) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})) β (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) |
126 | 2 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β π β β) |
127 | 5 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β π
β Fin) |
128 | 80 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β πΉ:π
βΆβ) |
129 | 6 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β πΊ:π
βΆβ0) |
130 | 7 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β ((π β 1) Ramsey πΊ) β
β0) |
131 | 8 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β π β Fin) |
132 | 29 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β (β―βπ) = (((π β 1) Ramsey πΊ) + 1)) |
133 | 33 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β πΎ:(ππΆπ)βΆπ
) |
134 | 19 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β π β π) |
135 | 82 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β π β π
) |
136 | 110 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β π€ β (π β {π})) |
137 | 106 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β (πΊβπ) β€ (β―βπ€)) |
138 | | simprrr 780 |
. . . . . . . . . . . 12
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β (π€πΆ(π β 1)) β (β‘π» β {π})) |
139 | 138 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β (π€πΆ(π β 1)) β (β‘π» β {π})) |
140 | | simprll 777 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β π β π
) |
141 | | simprlr 778 |
. . . . . . . . . . . 12
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β π£ β π« π€) |
142 | 141 | elpwid 4548 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β π£ β π€) |
143 | | simprrl 779 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£)) |
144 | | simprrr 780 |
. . . . . . . . . . . 12
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})) |
145 | | cnvresima 6144 |
. . . . . . . . . . . . 13
β’ (β‘(πΎ βΎ (π€πΆπ)) β {π}) = ((β‘πΎ β {π}) β© (π€πΆπ)) |
146 | | inss1 4168 |
. . . . . . . . . . . . 13
β’ ((β‘πΎ β {π}) β© (π€πΆπ)) β (β‘πΎ β {π}) |
147 | 145, 146 | eqsstri 3960 |
. . . . . . . . . . . 12
β’ (β‘(πΎ βΎ (π€πΆπ)) β {π}) β (β‘πΎ β {π}) |
148 | 144, 147 | sstrdi 3938 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β (π£πΆπ) β (β‘πΎ β {π})) |
149 | 126, 127,
128, 98, 129, 130, 1, 131, 132, 133, 134, 75, 135, 136, 137, 139, 140, 142, 143, 148 | ramub1lem1 16768 |
. . . . . . . . . 10
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ ((π β π
β§ π£ β π« π€) β§ (if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})))) β βπ§ β π« π((πΉβπ) β€ (β―βπ§) β§ (π§πΆπ) β (β‘πΎ β {π}))) |
150 | 149 | expr 458 |
. . . . . . . . 9
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ (π β π
β§ π£ β π« π€)) β ((if(π = π, ((πΉβπ) β 1), (πΉβπ)) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})) β βπ§ β π« π((πΉβπ) β€ (β―βπ§) β§ (π§πΆπ) β (β‘πΎ β {π})))) |
151 | 125, 150 | sylbid 240 |
. . . . . . . 8
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ (π β π
β§ π£ β π« π€)) β ((((π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦)))βπ) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})) β βπ§ β π« π((πΉβπ) β€ (β―βπ§) β§ (π§πΆπ) β (β‘πΎ β {π})))) |
152 | 151 | anassrs 469 |
. . . . . . 7
β’ ((((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ π β π
) β§ π£ β π« π€) β ((((π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦)))βπ) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})) β βπ§ β π« π((πΉβπ) β€ (β―βπ§) β§ (π§πΆπ) β (β‘πΎ β {π})))) |
153 | 152 | rexlimdva 3149 |
. . . . . 6
β’ (((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β§ π β π
) β (βπ£ β π« π€(((π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦)))βπ) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})) β βπ§ β π« π((πΉβπ) β€ (β―βπ§) β§ (π§πΆπ) β (β‘πΎ β {π})))) |
154 | 153 | reximdva 3162 |
. . . . 5
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β (βπ β π
βπ£ β π« π€(((π¦ β π
β¦ if(π¦ = π, ((πΉβπ) β 1), (πΉβπ¦)))βπ) β€ (β―βπ£) β§ (π£πΆπ) β (β‘(πΎ βΎ (π€πΆπ)) β {π})) β βπ β π
βπ§ β π« π((πΉβπ) β€ (β―βπ§) β§ (π§πΆπ) β (β‘πΎ β {π})))) |
155 | 115, 154 | mpd 15 |
. . . 4
β’ ((π β§ ((π β π
β§ π€ β π« (π β {π})) β§ ((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})))) β βπ β π
βπ§ β π« π((πΉβπ) β€ (β―βπ§) β§ (π§πΆπ) β (β‘πΎ β {π}))) |
156 | 155 | expr 458 |
. . 3
β’ ((π β§ (π β π
β§ π€ β π« (π β {π}))) β (((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})) β βπ β π
βπ§ β π« π((πΉβπ) β€ (β―βπ§) β§ (π§πΆπ) β (β‘πΎ β {π})))) |
157 | 156 | rexlimdvva 3202 |
. 2
β’ (π β (βπ β π
βπ€ β π« (π β {π})((πΊβπ) β€ (β―βπ€) β§ (π€πΆ(π β 1)) β (β‘π» β {π})) β βπ β π
βπ§ β π« π((πΉβπ) β€ (β―βπ§) β§ (π§πΆπ) β (β‘πΎ β {π})))) |
158 | 77, 157 | mpd 15 |
1
β’ (π β βπ β π
βπ§ β π« π((πΉβπ) β€ (β―βπ§) β§ (π§πΆπ) β (β‘πΎ β {π}))) |