Step | Hyp | Ref
| Expression |
1 | | fveqeq2 6901 |
. . . . . 6
β’ (π = ran π§ β ((β―βπ) = πΎ β (β―βran π§) = πΎ)) |
2 | | fzfid 13938 |
. . . . . . 7
β’ ((π β§ π§ β π΄) β (1...π) β Fin) |
3 | | eleq1w 2817 |
. . . . . . . . . . . . 13
β’ (π = π§ β (π β π΄ β π§ β π΄)) |
4 | | feq1 6699 |
. . . . . . . . . . . . . 14
β’ (π = π§ β (π:(1...πΎ)βΆ(1...π) β π§:(1...πΎ)βΆ(1...π))) |
5 | | fveq1 6891 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π§ β (πβπ₯) = (π§βπ₯)) |
6 | | fveq1 6891 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π§ β (πβπ¦) = (π§βπ¦)) |
7 | 5, 6 | breq12d 5162 |
. . . . . . . . . . . . . . . . 17
β’ (π = π§ β ((πβπ₯) < (πβπ¦) β (π§βπ₯) < (π§βπ¦))) |
8 | 7 | imbi2d 341 |
. . . . . . . . . . . . . . . 16
β’ (π = π§ β ((π₯ < π¦ β (πβπ₯) < (πβπ¦)) β (π₯ < π¦ β (π§βπ₯) < (π§βπ¦)))) |
9 | 8 | ralbidv 3178 |
. . . . . . . . . . . . . . 15
β’ (π = π§ β (βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)) β βπ¦ β (1...πΎ)(π₯ < π¦ β (π§βπ₯) < (π§βπ¦)))) |
10 | 9 | ralbidv 3178 |
. . . . . . . . . . . . . 14
β’ (π = π§ β (βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)) β βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (π§βπ₯) < (π§βπ¦)))) |
11 | 4, 10 | anbi12d 632 |
. . . . . . . . . . . . 13
β’ (π = π§ β ((π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦))) β (π§:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (π§βπ₯) < (π§βπ¦))))) |
12 | 3, 11 | bibi12d 346 |
. . . . . . . . . . . 12
β’ (π = π§ β ((π β π΄ β (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) β (π§ β π΄ β (π§:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (π§βπ₯) < (π§βπ¦)))))) |
13 | | sticksstones2.4 |
. . . . . . . . . . . . . 14
β’ π΄ = {π β£ (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))} |
14 | | eqabb 2874 |
. . . . . . . . . . . . . 14
β’ (π΄ = {π β£ (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))} β βπ(π β π΄ β (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦))))) |
15 | 13, 14 | mpbi 229 |
. . . . . . . . . . . . 13
β’
βπ(π β π΄ β (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
16 | 15 | spi 2178 |
. . . . . . . . . . . 12
β’ (π β π΄ β (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
17 | 12, 16 | chvarvv 2003 |
. . . . . . . . . . 11
β’ (π§ β π΄ β (π§:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (π§βπ₯) < (π§βπ¦)))) |
18 | 17 | biimpi 215 |
. . . . . . . . . 10
β’ (π§ β π΄ β (π§:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (π§βπ₯) < (π§βπ¦)))) |
19 | 18 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π§ β π΄) β (π§:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (π§βπ₯) < (π§βπ¦)))) |
20 | 19 | simpld 496 |
. . . . . . . 8
β’ ((π β§ π§ β π΄) β π§:(1...πΎ)βΆ(1...π)) |
21 | 20 | frnd 6726 |
. . . . . . 7
β’ ((π β§ π§ β π΄) β ran π§ β (1...π)) |
22 | 2, 21 | sselpwd 5327 |
. . . . . 6
β’ ((π β§ π§ β π΄) β ran π§ β π« (1...π)) |
23 | 20 | ffnd 6719 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π΄) β π§ Fn (1...πΎ)) |
24 | | hashfn 14335 |
. . . . . . . . . . 11
β’ (π§ Fn (1...πΎ) β (β―βπ§) = (β―β(1...πΎ))) |
25 | 23, 24 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π§ β π΄) β (β―βπ§) = (β―β(1...πΎ))) |
26 | | sticksstones2.2 |
. . . . . . . . . . . 12
β’ (π β πΎ β
β0) |
27 | 26 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π΄) β πΎ β
β0) |
28 | | hashfz1 14306 |
. . . . . . . . . . 11
β’ (πΎ β β0
β (β―β(1...πΎ)) = πΎ) |
29 | 27, 28 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π§ β π΄) β (β―β(1...πΎ)) = πΎ) |
30 | 25, 29 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β§ π§ β π΄) β (β―βπ§) = πΎ) |
31 | 30 | eqcomd 2739 |
. . . . . . . 8
β’ ((π β§ π§ β π΄) β πΎ = (β―βπ§)) |
32 | | fzfid 13938 |
. . . . . . . . 9
β’ ((π β§ π§ β π΄) β (1...πΎ) β Fin) |
33 | | elfznn 13530 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...πΎ) β π β β) |
34 | 33 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π§ β π΄ β§ π β (1...πΎ)) β π β β) |
35 | 34 | nnred 12227 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β π΄ β§ π β (1...πΎ)) β π β β) |
36 | 35 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β π β β) |
37 | | elfznn 13530 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...πΎ) β π β β) |
38 | 37 | nnred 12227 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...πΎ) β π β β) |
39 | 38 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β π β β) |
40 | | lttri2 11296 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β) β (π β π β (π < π β¨ π < π))) |
41 | 36, 39, 40 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β (π β π β (π < π β¨ π < π))) |
42 | 20 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π§ β π΄ β§ π β (1...πΎ)) β π§:(1...πΎ)βΆ(1...π)) |
43 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π§ β π΄ β§ π β (1...πΎ)) β π β (1...πΎ)) |
44 | 42, 43 | ffvelcdmd 7088 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π§ β π΄ β§ π β (1...πΎ)) β (π§βπ) β (1...π)) |
45 | 44 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β (π§βπ) β (1...π)) |
46 | 45 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β§ π < π) β (π§βπ) β (1...π)) |
47 | | elfznn 13530 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π§βπ) β (1...π) β (π§βπ) β β) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β§ π < π) β (π§βπ) β β) |
49 | 48 | nnred 12227 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β§ π < π) β (π§βπ) β β) |
50 | 19 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π§ β π΄) β βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (π§βπ₯) < (π§βπ¦))) |
51 | 50 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π§ β π΄ β§ π β (1...πΎ)) β βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (π§βπ₯) < (π§βπ¦))) |
52 | 51 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (π§βπ₯) < (π§βπ¦))) |
53 | 43 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β π β (1...πΎ)) |
54 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β π β (1...πΎ)) |
55 | | breq1 5152 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ = π β (π₯ < π¦ β π < π¦)) |
56 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ = π β (π§βπ₯) = (π§βπ)) |
57 | 56 | breq1d 5159 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ = π β ((π§βπ₯) < (π§βπ¦) β (π§βπ) < (π§βπ¦))) |
58 | 55, 57 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = π β ((π₯ < π¦ β (π§βπ₯) < (π§βπ¦)) β (π < π¦ β (π§βπ) < (π§βπ¦)))) |
59 | | breq2 5153 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π¦ = π β (π < π¦ β π < π)) |
60 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π¦ = π β (π§βπ¦) = (π§βπ)) |
61 | 60 | breq2d 5161 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π¦ = π β ((π§βπ) < (π§βπ¦) β (π§βπ) < (π§βπ))) |
62 | 59, 61 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π¦ = π β ((π < π¦ β (π§βπ) < (π§βπ¦)) β (π < π β (π§βπ) < (π§βπ)))) |
63 | 58, 62 | rspc2v 3623 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (1...πΎ) β§ π β (1...πΎ)) β (βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (π§βπ₯) < (π§βπ¦)) β (π < π β (π§βπ) < (π§βπ)))) |
64 | 53, 54, 63 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β (βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (π§βπ₯) < (π§βπ¦)) β (π < π β (π§βπ) < (π§βπ)))) |
65 | 52, 64 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β (π < π β (π§βπ) < (π§βπ))) |
66 | 65 | imp 408 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β§ π < π) β (π§βπ) < (π§βπ)) |
67 | 49, 66 | ltned 11350 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β§ π < π) β (π§βπ) β (π§βπ)) |
68 | 42 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β (π§βπ) β (1...π)) |
69 | | elfznn 13530 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π§βπ) β (1...π) β (π§βπ) β β) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β (π§βπ) β β) |
71 | 70 | nnred 12227 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β (π§βπ) β β) |
72 | 71 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β§ π < π) β (π§βπ) β β) |
73 | | breq1 5152 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ = π β (π₯ < π¦ β π < π¦)) |
74 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π₯ = π β (π§βπ₯) = (π§βπ)) |
75 | 74 | breq1d 5159 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ = π β ((π§βπ₯) < (π§βπ¦) β (π§βπ) < (π§βπ¦))) |
76 | 73, 75 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ = π β ((π₯ < π¦ β (π§βπ₯) < (π§βπ¦)) β (π < π¦ β (π§βπ) < (π§βπ¦)))) |
77 | | breq2 5153 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π¦ = π β (π < π¦ β π < π)) |
78 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ = π β (π§βπ¦) = (π§βπ)) |
79 | 78 | breq2d 5161 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π¦ = π β ((π§βπ) < (π§βπ¦) β (π§βπ) < (π§βπ))) |
80 | 77, 79 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π¦ = π β ((π < π¦ β (π§βπ) < (π§βπ¦)) β (π < π β (π§βπ) < (π§βπ)))) |
81 | 76, 80 | rspc2v 3623 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (1...πΎ) β§ π β (1...πΎ)) β (βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (π§βπ₯) < (π§βπ¦)) β (π < π β (π§βπ) < (π§βπ)))) |
82 | 54, 53, 81 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β (βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (π§βπ₯) < (π§βπ¦)) β (π < π β (π§βπ) < (π§βπ)))) |
83 | 52, 82 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β (π < π β (π§βπ) < (π§βπ))) |
84 | 83 | imp 408 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β§ π < π) β (π§βπ) < (π§βπ)) |
85 | 72, 84 | ltned 11350 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β§ π < π) β (π§βπ) β (π§βπ)) |
86 | 85 | necomd 2997 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β§ π < π) β (π§βπ) β (π§βπ)) |
87 | 67, 86 | jaodan 957 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β§ (π < π β¨ π < π)) β (π§βπ) β (π§βπ)) |
88 | 87 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β ((π < π β¨ π < π) β (π§βπ) β (π§βπ))) |
89 | 41, 88 | sylbid 239 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β (π β π β (π§βπ) β (π§βπ))) |
90 | 89 | necon4d 2965 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β π΄ β§ π β (1...πΎ)) β§ π β (1...πΎ)) β ((π§βπ) = (π§βπ) β π = π)) |
91 | 90 | ralrimiva 3147 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π΄ β§ π β (1...πΎ)) β βπ β (1...πΎ)((π§βπ) = (π§βπ) β π = π)) |
92 | 91 | 3expa 1119 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π΄) β§ π β (1...πΎ)) β βπ β (1...πΎ)((π§βπ) = (π§βπ) β π = π)) |
93 | 92 | ralrimiva 3147 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π΄) β βπ β (1...πΎ)βπ β (1...πΎ)((π§βπ) = (π§βπ) β π = π)) |
94 | 20, 93 | jca 513 |
. . . . . . . . . 10
β’ ((π β§ π§ β π΄) β (π§:(1...πΎ)βΆ(1...π) β§ βπ β (1...πΎ)βπ β (1...πΎ)((π§βπ) = (π§βπ) β π = π))) |
95 | | dff13 7254 |
. . . . . . . . . 10
β’ (π§:(1...πΎ)β1-1β(1...π) β (π§:(1...πΎ)βΆ(1...π) β§ βπ β (1...πΎ)βπ β (1...πΎ)((π§βπ) = (π§βπ) β π = π))) |
96 | 94, 95 | sylibr 233 |
. . . . . . . . 9
β’ ((π β§ π§ β π΄) β π§:(1...πΎ)β1-1β(1...π)) |
97 | | hashf1rn 14312 |
. . . . . . . . 9
β’
(((1...πΎ) β Fin
β§ π§:(1...πΎ)β1-1β(1...π)) β (β―βπ§) = (β―βran π§)) |
98 | 32, 96, 97 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π§ β π΄) β (β―βπ§) = (β―βran π§)) |
99 | 31, 98 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ π§ β π΄) β πΎ = (β―βran π§)) |
100 | 99 | eqcomd 2739 |
. . . . . 6
β’ ((π β§ π§ β π΄) β (β―βran π§) = πΎ) |
101 | 1, 22, 100 | elrabd 3686 |
. . . . 5
β’ ((π β§ π§ β π΄) β ran π§ β {π β π« (1...π) β£ (β―βπ) = πΎ}) |
102 | | sticksstones2.3 |
. . . . . . 7
β’ π΅ = {π β π« (1...π) β£ (β―βπ) = πΎ} |
103 | 102 | eleq2i 2826 |
. . . . . 6
β’ (ran
π§ β π΅ β ran π§ β {π β π« (1...π) β£ (β―βπ) = πΎ}) |
104 | 103 | a1i 11 |
. . . . 5
β’ ((π β§ π§ β π΄) β (ran π§ β π΅ β ran π§ β {π β π« (1...π) β£ (β―βπ) = πΎ})) |
105 | 101, 104 | mpbird 257 |
. . . 4
β’ ((π β§ π§ β π΄) β ran π§ β π΅) |
106 | | sticksstones2.5 |
. . . 4
β’ πΉ = (π§ β π΄ β¦ ran π§) |
107 | 105, 106 | fmptd 7114 |
. . 3
β’ (π β πΉ:π΄βΆπ΅) |
108 | | sticksstones2.1 |
. . . . . . . . . . . 12
β’ (π β π β
β0) |
109 | 108 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄ β§ π β π΄) β π β
β0) |
110 | 109 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β π΄ β§ π β π΄) β§ π β π) β π β
β0) |
111 | 26 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄ β§ π β π΄) β πΎ β
β0) |
112 | 111 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β π΄ β§ π β π΄) β§ π β π) β πΎ β
β0) |
113 | | simpl2 1193 |
. . . . . . . . . 10
β’ (((π β§ π β π΄ β§ π β π΄) β§ π β π) β π β π΄) |
114 | | simpl3 1194 |
. . . . . . . . . 10
β’ (((π β§ π β π΄ β§ π β π΄) β§ π β π) β π β π΄) |
115 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π β π΄ β§ π β π΄) β§ π β π) β π β π) |
116 | | fveq2 6892 |
. . . . . . . . . . . . 13
β’ (π = π β (πβπ) = (πβπ )) |
117 | | fveq2 6892 |
. . . . . . . . . . . . 13
β’ (π = π β (πβπ) = (πβπ )) |
118 | 116, 117 | neeq12d 3003 |
. . . . . . . . . . . 12
β’ (π = π β ((πβπ) β (πβπ) β (πβπ ) β (πβπ ))) |
119 | 118 | cbvrabv 3443 |
. . . . . . . . . . 11
β’ {π β (1...πΎ) β£ (πβπ) β (πβπ)} = {π β (1...πΎ) β£ (πβπ ) β (πβπ )} |
120 | 119 | infeq1i 9473 |
. . . . . . . . . 10
β’
inf({π β
(1...πΎ) β£ (πβπ) β (πβπ)}, β, < ) = inf({π β (1...πΎ) β£ (πβπ ) β (πβπ )}, β, < ) |
121 | 110, 112,
13, 113, 114, 115, 120 | sticksstones1 40962 |
. . . . . . . . 9
β’ (((π β§ π β π΄ β§ π β π΄) β§ π β π) β ran π β ran π) |
122 | 106 | a1i 11 |
. . . . . . . . . 10
β’ (((π β§ π β π΄ β§ π β π΄) β§ π β π) β πΉ = (π§ β π΄ β¦ ran π§)) |
123 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄ β§ π β π΄) β§ π β π) β§ π§ = π) β π§ = π) |
124 | 123 | rneqd 5938 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄ β§ π β π΄) β§ π β π) β§ π§ = π) β ran π§ = ran π) |
125 | | fzfid 13938 |
. . . . . . . . . . 11
β’ (((π β§ π β π΄ β§ π β π΄) β§ π β π) β (1...π) β Fin) |
126 | | eleq1w 2817 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (π β π΄ β π β π΄)) |
127 | | feq1 6699 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (π:(1...πΎ)βΆ(1...π) β π:(1...πΎ)βΆ(1...π))) |
128 | | fveq1 6891 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (πβπ₯) = (πβπ₯)) |
129 | | fveq1 6891 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (πβπ¦) = (πβπ¦)) |
130 | 128, 129 | breq12d 5162 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β ((πβπ₯) < (πβπ¦) β (πβπ₯) < (πβπ¦))) |
131 | 130 | imbi2d 341 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((π₯ < π¦ β (πβπ₯) < (πβπ¦)) β (π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
132 | 131 | 2ralbidv 3219 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)) β βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
133 | 127, 132 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦))) β (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦))))) |
134 | 126, 133 | bibi12d 346 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((π β π΄ β (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) β (π β π΄ β (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))))) |
135 | 134, 16 | chvarvv 2003 |
. . . . . . . . . . . . . . . . 17
β’ (π β π΄ β (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
136 | 135 | biimpi 215 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
137 | 136 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
138 | 137 | simpld 496 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β π:(1...πΎ)βΆ(1...π)) |
139 | 138 | 3adant3 1133 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄ β§ π β π΄) β π:(1...πΎ)βΆ(1...π)) |
140 | 139 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄ β§ π β π΄) β§ π β π) β π:(1...πΎ)βΆ(1...π)) |
141 | 140 | frnd 6726 |
. . . . . . . . . . 11
β’ (((π β§ π β π΄ β§ π β π΄) β§ π β π) β ran π β (1...π)) |
142 | 125, 141 | sselpwd 5327 |
. . . . . . . . . 10
β’ (((π β§ π β π΄ β§ π β π΄) β§ π β π) β ran π β π« (1...π)) |
143 | 122, 124,
113, 142 | fvmptd 7006 |
. . . . . . . . 9
β’ (((π β§ π β π΄ β§ π β π΄) β§ π β π) β (πΉβπ) = ran π) |
144 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄ β§ π β π΄) β§ π β π) β§ π§ = π) β π§ = π) |
145 | 144 | rneqd 5938 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄ β§ π β π΄) β§ π β π) β§ π§ = π) β ran π§ = ran π) |
146 | | fzfid 13938 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β Fin) |
147 | 146 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄ β§ π β π΄) β (1...π) β Fin) |
148 | | eleq1w 2817 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (π β π΄ β π β π΄)) |
149 | | feq1 6699 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (π:(1...πΎ)βΆ(1...π) β π:(1...πΎ)βΆ(1...π))) |
150 | | fveq1 6891 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (πβπ₯) = (πβπ₯)) |
151 | | fveq1 6891 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (πβπ¦) = (πβπ¦)) |
152 | 150, 151 | breq12d 5162 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β ((πβπ₯) < (πβπ¦) β (πβπ₯) < (πβπ¦))) |
153 | 152 | imbi2d 341 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((π₯ < π¦ β (πβπ₯) < (πβπ¦)) β (π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
154 | 153 | 2ralbidv 3219 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)) β βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
155 | 149, 154 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦))) β (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦))))) |
156 | 148, 155 | bibi12d 346 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((π β π΄ β (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) β (π β π΄ β (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))))) |
157 | 156, 16 | chvarvv 2003 |
. . . . . . . . . . . . . . . . 17
β’ (π β π΄ β (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
158 | 157 | biimpi 215 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
159 | 158 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β (π:(1...πΎ)βΆ(1...π) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
160 | 159 | simpld 496 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β π:(1...πΎ)βΆ(1...π)) |
161 | 160 | 3adant2 1132 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄ β§ π β π΄) β π:(1...πΎ)βΆ(1...π)) |
162 | 161 | frnd 6726 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄ β§ π β π΄) β ran π β (1...π)) |
163 | 147, 162 | sselpwd 5327 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄ β§ π β π΄) β ran π β π« (1...π)) |
164 | 163 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β π΄ β§ π β π΄) β§ π β π) β ran π β π« (1...π)) |
165 | 122, 145,
114, 164 | fvmptd 7006 |
. . . . . . . . 9
β’ (((π β§ π β π΄ β§ π β π΄) β§ π β π) β (πΉβπ) = ran π) |
166 | 121, 143,
165 | 3netr4d 3019 |
. . . . . . . 8
β’ (((π β§ π β π΄ β§ π β π΄) β§ π β π) β (πΉβπ) β (πΉβπ)) |
167 | 166 | ex 414 |
. . . . . . 7
β’ ((π β§ π β π΄ β§ π β π΄) β (π β π β (πΉβπ) β (πΉβπ))) |
168 | 167 | necon4d 2965 |
. . . . . 6
β’ ((π β§ π β π΄ β§ π β π΄) β ((πΉβπ) = (πΉβπ) β π = π)) |
169 | 168 | 3expa 1119 |
. . . . 5
β’ (((π β§ π β π΄) β§ π β π΄) β ((πΉβπ) = (πΉβπ) β π = π)) |
170 | 169 | ralrimiva 3147 |
. . . 4
β’ ((π β§ π β π΄) β βπ β π΄ ((πΉβπ) = (πΉβπ) β π = π)) |
171 | 170 | ralrimiva 3147 |
. . 3
β’ (π β βπ β π΄ βπ β π΄ ((πΉβπ) = (πΉβπ) β π = π)) |
172 | 107, 171 | jca 513 |
. 2
β’ (π β (πΉ:π΄βΆπ΅ β§ βπ β π΄ βπ β π΄ ((πΉβπ) = (πΉβπ) β π = π))) |
173 | | dff13 7254 |
. 2
β’ (πΉ:π΄β1-1βπ΅ β (πΉ:π΄βΆπ΅ β§ βπ β π΄ βπ β π΄ ((πΉβπ) = (πΉβπ) β π = π))) |
174 | 172, 173 | sylibr 233 |
1
β’ (π β πΉ:π΄β1-1βπ΅) |