Step | Hyp | Ref
| Expression |
1 | | vdw.r |
. . 3
β’ (π β π
β Fin) |
2 | | vdwlem9.k |
. . 3
β’ (π β πΎ β
(β€β₯β2)) |
3 | | vdwlem9.s |
. . 3
β’ (π β βπ β Fin βπ β β βπ β (π βm (1...π))πΎ MonoAP π) |
4 | | hashcl 14316 |
. . . . 5
β’ (π
β Fin β
(β―βπ
) β
β0) |
5 | 1, 4 | syl 17 |
. . . 4
β’ (π β (β―βπ
) β
β0) |
6 | | nn0p1nn 12511 |
. . . 4
β’
((β―βπ
)
β β0 β ((β―βπ
) + 1) β β) |
7 | 5, 6 | syl 17 |
. . 3
β’ (π β ((β―βπ
) + 1) β
β) |
8 | 1, 2, 3, 7 | vdwlem10 16923 |
. 2
β’ (π β βπ β β βπ β (π
βm (1...π))(β¨((β―βπ
) + 1), πΎβ© PolyAP π β¨ (πΎ + 1) MonoAP π)) |
9 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β π
β Fin) |
10 | | ovex 7442 |
. . . . . . 7
β’
(1...π) β
V |
11 | | elmapg 8833 |
. . . . . . 7
β’ ((π
β Fin β§ (1...π) β V) β (π β (π
βm (1...π)) β π:(1...π)βΆπ
)) |
12 | 9, 10, 11 | sylancl 587 |
. . . . . 6
β’ ((π β§ π β β) β (π β (π
βm (1...π)) β π:(1...π)βΆπ
)) |
13 | 12 | biimpa 478 |
. . . . 5
β’ (((π β§ π β β) β§ π β (π
βm (1...π))) β π:(1...π)βΆπ
) |
14 | 5 | nn0red 12533 |
. . . . . . . . . . 11
β’ (π β (β―βπ
) β
β) |
15 | 14 | ltp1d 12144 |
. . . . . . . . . 10
β’ (π β (β―βπ
) < ((β―βπ
) + 1)) |
16 | | peano2re 11387 |
. . . . . . . . . . . 12
β’
((β―βπ
)
β β β ((β―βπ
) + 1) β β) |
17 | 14, 16 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((β―βπ
) + 1) β
β) |
18 | 14, 17 | ltnled 11361 |
. . . . . . . . . 10
β’ (π β ((β―βπ
) < ((β―βπ
) + 1) β Β¬
((β―βπ
) + 1)
β€ (β―βπ
))) |
19 | 15, 18 | mpbid 231 |
. . . . . . . . 9
β’ (π β Β¬
((β―βπ
) + 1)
β€ (β―βπ
)) |
20 | 19 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β β β§ π:(1...π)βΆπ
)) β Β¬ ((β―βπ
) + 1) β€ (β―βπ
)) |
21 | | eluz2nn 12868 |
. . . . . . . . . . . . 13
β’ (πΎ β
(β€β₯β2) β πΎ β β) |
22 | 2, 21 | syl 17 |
. . . . . . . . . . . 12
β’ (π β πΎ β β) |
23 | 22 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ π:(1...π)βΆπ
)) β πΎ β β) |
24 | 23 | nnnn0d 12532 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ π:(1...π)βΆπ
)) β πΎ β
β0) |
25 | | simprr 772 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ π:(1...π)βΆπ
)) β π:(1...π)βΆπ
) |
26 | 7 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ π:(1...π)βΆπ
)) β ((β―βπ
) + 1) β β) |
27 | | eqid 2733 |
. . . . . . . . . 10
β’
(1...((β―βπ
) + 1)) = (1...((β―βπ
) + 1)) |
28 | 10, 24, 25, 26, 27 | vdwpc 16913 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ π:(1...π)βΆπ
)) β (β¨((β―βπ
) + 1), πΎβ© PolyAP π β βπ β β βπ β (β βm
(1...((β―βπ
) +
1)))(βπ β
(1...((β―βπ
) +
1))((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) β§ (β―βran (π β
(1...((β―βπ
) +
1)) β¦ (πβ(π + (πβπ))))) = ((β―βπ
) + 1)))) |
29 | 1 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ βπ
β (1...((β―βπ
) + 1))((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))})) β π
β Fin) |
30 | 25 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ π β
(1...((β―βπ
) +
1))) β π:(1...π)βΆπ
) |
31 | 25 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ π β
(1...((β―βπ
) +
1))) β§ ((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))})) β π:(1...π)βΆπ
) |
32 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ π β
(1...((β―βπ
) +
1))) β§ ((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))})) β ((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))})) |
33 | | cnvimass 6081 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β‘π β {(πβ(π + (πβπ)))}) β dom π |
34 | 32, 33 | sstrdi 3995 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ π β
(1...((β―βπ
) +
1))) β§ ((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))})) β ((π + (πβπ))(APβπΎ)(πβπ)) β dom π) |
35 | 31, 34 | fssdmd 6737 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ π β
(1...((β―βπ
) +
1))) β§ ((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))})) β ((π + (πβπ))(APβπΎ)(πβπ)) β (1...π)) |
36 | 22 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ π β
(1...((β―βπ
) +
1))) β πΎ β
β) |
37 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ π β
(1...((β―βπ
) +
1))) β π β
β) |
38 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β π β
(β βm (1...((β―βπ
) + 1)))) |
39 | | nnex 12218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ β
β V |
40 | | ovex 7442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(1...((β―βπ
) + 1)) β V |
41 | 39, 40 | elmap 8865 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (β
βm (1...((β―βπ
) + 1))) β π:(1...((β―βπ
) + 1))βΆβ) |
42 | 38, 41 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β π:(1...((β―βπ
) + 1))βΆβ) |
43 | 42 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ π β
(1...((β―βπ
) +
1))) β (πβπ) β
β) |
44 | 37, 43 | nnaddcld 12264 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ π β
(1...((β―βπ
) +
1))) β (π + (πβπ)) β β) |
45 | | vdwapid1 16908 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΎ β β β§ (π + (πβπ)) β β β§ (πβπ) β β) β (π + (πβπ)) β ((π + (πβπ))(APβπΎ)(πβπ))) |
46 | 36, 44, 43, 45 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ π β
(1...((β―βπ
) +
1))) β (π + (πβπ)) β ((π + (πβπ))(APβπΎ)(πβπ))) |
47 | 46 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ π β
(1...((β―βπ
) +
1))) β§ ((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))})) β (π + (πβπ)) β ((π + (πβπ))(APβπΎ)(πβπ))) |
48 | 35, 47 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ π β
(1...((β―βπ
) +
1))) β§ ((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))})) β (π + (πβπ)) β (1...π)) |
49 | 48 | ex 414 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ π β
(1...((β―βπ
) +
1))) β (((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) β (π + (πβπ)) β (1...π))) |
50 | | ffvelcdm 7084 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π:(1...π)βΆπ
β§ (π + (πβπ)) β (1...π)) β (πβ(π + (πβπ))) β π
) |
51 | 30, 49, 50 | syl6an 683 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ π β
(1...((β―βπ
) +
1))) β (((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) β (πβ(π + (πβπ))) β π
)) |
52 | 51 | ralimdva 3168 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β (βπ
β (1...((β―βπ
) + 1))((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) β βπ β (1...((β―βπ
) + 1))(πβ(π + (πβπ))) β π
)) |
53 | 52 | imp 408 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ βπ
β (1...((β―βπ
) + 1))((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))})) β βπ β (1...((β―βπ
) + 1))(πβ(π + (πβπ))) β π
) |
54 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(1...((β―βπ
) +
1)) β¦ (πβ(π + (πβπ)))) = (π β (1...((β―βπ
) + 1)) β¦ (πβ(π + (πβπ)))) |
55 | 54 | fmpt 7110 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
(1...((β―βπ
) +
1))(πβ(π + (πβπ))) β π
β (π β (1...((β―βπ
) + 1)) β¦ (πβ(π + (πβπ)))):(1...((β―βπ
) + 1))βΆπ
) |
56 | 53, 55 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ βπ
β (1...((β―βπ
) + 1))((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))})) β (π β (1...((β―βπ
) + 1)) β¦ (πβ(π + (πβπ)))):(1...((β―βπ
) + 1))βΆπ
) |
57 | 56 | frnd 6726 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ βπ
β (1...((β―βπ
) + 1))((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))})) β ran (π β (1...((β―βπ
) + 1)) β¦ (πβ(π + (πβπ)))) β π
) |
58 | | ssdomg 8996 |
. . . . . . . . . . . . . 14
β’ (π
β Fin β (ran (π β
(1...((β―βπ
) +
1)) β¦ (πβ(π + (πβπ)))) β π
β ran (π β (1...((β―βπ
) + 1)) β¦ (πβ(π + (πβπ)))) βΌ π
)) |
59 | 29, 57, 58 | sylc 65 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ βπ
β (1...((β―βπ
) + 1))((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))})) β ran (π β (1...((β―βπ
) + 1)) β¦ (πβ(π + (πβπ)))) βΌ π
) |
60 | 29, 57 | ssfid 9267 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ βπ
β (1...((β―βπ
) + 1))((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))})) β ran (π β (1...((β―βπ
) + 1)) β¦ (πβ(π + (πβπ)))) β Fin) |
61 | | hashdom 14339 |
. . . . . . . . . . . . . 14
β’ ((ran
(π β
(1...((β―βπ
) +
1)) β¦ (πβ(π + (πβπ)))) β Fin β§ π
β Fin) β ((β―βran
(π β
(1...((β―βπ
) +
1)) β¦ (πβ(π + (πβπ))))) β€ (β―βπ
) β ran (π β (1...((β―βπ
) + 1)) β¦ (πβ(π + (πβπ)))) βΌ π
)) |
62 | 60, 29, 61 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ βπ
β (1...((β―βπ
) + 1))((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))})) β ((β―βran (π β
(1...((β―βπ
) +
1)) β¦ (πβ(π + (πβπ))))) β€ (β―βπ
) β ran (π β (1...((β―βπ
) + 1)) β¦ (πβ(π + (πβπ)))) βΌ π
)) |
63 | 59, 62 | mpbird 257 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ βπ
β (1...((β―βπ
) + 1))((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))})) β (β―βran (π β
(1...((β―βπ
) +
1)) β¦ (πβ(π + (πβπ))))) β€ (β―βπ
)) |
64 | | breq1 5152 |
. . . . . . . . . . . 12
β’
((β―βran (π β (1...((β―βπ
) + 1)) β¦ (πβ(π + (πβπ))))) = ((β―βπ
) + 1) β ((β―βran (π β
(1...((β―βπ
) +
1)) β¦ (πβ(π + (πβπ))))) β€ (β―βπ
) β ((β―βπ
) + 1) β€ (β―βπ
))) |
65 | 63, 64 | syl5ibcom 244 |
. . . . . . . . . . 11
β’ ((((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β§ βπ
β (1...((β―βπ
) + 1))((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))})) β ((β―βran (π β
(1...((β―βπ
) +
1)) β¦ (πβ(π + (πβπ))))) = ((β―βπ
) + 1) β ((β―βπ
) + 1) β€ (β―βπ
))) |
66 | 65 | expimpd 455 |
. . . . . . . . . 10
β’ (((π β§ (π β β β§ π:(1...π)βΆπ
)) β§ (π β β β§ π β (β βm
(1...((β―βπ
) +
1))))) β ((βπ
β (1...((β―βπ
) + 1))((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) β§ (β―βran (π β
(1...((β―βπ
) +
1)) β¦ (πβ(π + (πβπ))))) = ((β―βπ
) + 1)) β ((β―βπ
) + 1) β€ (β―βπ
))) |
67 | 66 | rexlimdvva 3212 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ π:(1...π)βΆπ
)) β (βπ β β βπ β (β βm
(1...((β―βπ
) +
1)))(βπ β
(1...((β―βπ
) +
1))((π + (πβπ))(APβπΎ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) β§ (β―βran (π β
(1...((β―βπ
) +
1)) β¦ (πβ(π + (πβπ))))) = ((β―βπ
) + 1)) β ((β―βπ
) + 1) β€ (β―βπ
))) |
68 | 28, 67 | sylbid 239 |
. . . . . . . 8
β’ ((π β§ (π β β β§ π:(1...π)βΆπ
)) β (β¨((β―βπ
) + 1), πΎβ© PolyAP π β ((β―βπ
) + 1) β€ (β―βπ
))) |
69 | 20, 68 | mtod 197 |
. . . . . . 7
β’ ((π β§ (π β β β§ π:(1...π)βΆπ
)) β Β¬ β¨((β―βπ
) + 1), πΎβ© PolyAP π) |
70 | | biorf 936 |
. . . . . . 7
β’ (Β¬
β¨((β―βπ
) +
1), πΎβ© PolyAP π β ((πΎ + 1) MonoAP π β (β¨((β―βπ
) + 1), πΎβ© PolyAP π β¨ (πΎ + 1) MonoAP π))) |
71 | 69, 70 | syl 17 |
. . . . . 6
β’ ((π β§ (π β β β§ π:(1...π)βΆπ
)) β ((πΎ + 1) MonoAP π β (β¨((β―βπ
) + 1), πΎβ© PolyAP π β¨ (πΎ + 1) MonoAP π))) |
72 | 71 | anassrs 469 |
. . . . 5
β’ (((π β§ π β β) β§ π:(1...π)βΆπ
) β ((πΎ + 1) MonoAP π β (β¨((β―βπ
) + 1), πΎβ© PolyAP π β¨ (πΎ + 1) MonoAP π))) |
73 | 13, 72 | syldan 592 |
. . . 4
β’ (((π β§ π β β) β§ π β (π
βm (1...π))) β ((πΎ + 1) MonoAP π β (β¨((β―βπ
) + 1), πΎβ© PolyAP π β¨ (πΎ + 1) MonoAP π))) |
74 | 73 | ralbidva 3176 |
. . 3
β’ ((π β§ π β β) β (βπ β (π
βm (1...π))(πΎ + 1) MonoAP π β βπ β (π
βm (1...π))(β¨((β―βπ
) + 1), πΎβ© PolyAP π β¨ (πΎ + 1) MonoAP π))) |
75 | 74 | rexbidva 3177 |
. 2
β’ (π β (βπ β β βπ β (π
βm (1...π))(πΎ + 1) MonoAP π β βπ β β βπ β (π
βm (1...π))(β¨((β―βπ
) + 1), πΎβ© PolyAP π β¨ (πΎ + 1) MonoAP π))) |
76 | 8, 75 | mpbird 257 |
1
β’ (π β βπ β β βπ β (π
βm (1...π))(πΎ + 1) MonoAP π) |