Step | Hyp | Ref
| Expression |
1 | | znle2.y |
. . . . 5
β’ π =
(β€/nβ€βπ) |
2 | 1 | fvexi 6860 |
. . . 4
β’ π β V |
3 | 2 | a1i 11 |
. . 3
β’ (π β β0
β π β
V) |
4 | | znleval.x |
. . . 4
β’ π = (Baseβπ) |
5 | 4 | a1i 11 |
. . 3
β’ (π β β0
β π =
(Baseβπ)) |
6 | | znle2.l |
. . . 4
β’ β€ =
(leβπ) |
7 | 6 | a1i 11 |
. . 3
β’ (π β β0
β β€ = (leβπ)) |
8 | | znle2.f |
. . . . . . . . . 10
β’ πΉ = ((β€RHomβπ) βΎ π) |
9 | | znle2.w |
. . . . . . . . . 10
β’ π = if(π = 0, β€, (0..^π)) |
10 | 1, 4, 8, 9 | znf1o 20981 |
. . . . . . . . 9
β’ (π β β0
β πΉ:πβ1-1-ontoβπ) |
11 | | f1ocnv 6800 |
. . . . . . . . 9
β’ (πΉ:πβ1-1-ontoβπ β β‘πΉ:πβ1-1-ontoβπ) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
β’ (π β β0
β β‘πΉ:πβ1-1-ontoβπ) |
13 | | f1of 6788 |
. . . . . . . 8
β’ (β‘πΉ:πβ1-1-ontoβπ β β‘πΉ:πβΆπ) |
14 | 12, 13 | syl 17 |
. . . . . . 7
β’ (π β β0
β β‘πΉ:πβΆπ) |
15 | | sseq1 3973 |
. . . . . . . . . 10
β’ (β€
= if(π = 0, β€,
(0..^π)) β (β€
β β€ β if(π
= 0, β€, (0..^π))
β β€)) |
16 | | sseq1 3973 |
. . . . . . . . . 10
β’
((0..^π) = if(π = 0, β€, (0..^π)) β ((0..^π) β β€ β
if(π = 0, β€,
(0..^π)) β
β€)) |
17 | | ssid 3970 |
. . . . . . . . . 10
β’ β€
β β€ |
18 | | fzossz 13601 |
. . . . . . . . . 10
β’
(0..^π) β
β€ |
19 | 15, 16, 17, 18 | keephyp 4561 |
. . . . . . . . 9
β’ if(π = 0, β€, (0..^π)) β
β€ |
20 | 9, 19 | eqsstri 3982 |
. . . . . . . 8
β’ π β
β€ |
21 | | zssre 12514 |
. . . . . . . 8
β’ β€
β β |
22 | 20, 21 | sstri 3957 |
. . . . . . 7
β’ π β
β |
23 | | fss 6689 |
. . . . . . 7
β’ ((β‘πΉ:πβΆπ β§ π β β) β β‘πΉ:πβΆβ) |
24 | 14, 22, 23 | sylancl 587 |
. . . . . 6
β’ (π β β0
β β‘πΉ:πβΆβ) |
25 | 24 | ffvelcdmda 7039 |
. . . . 5
β’ ((π β β0
β§ π₯ β π) β (β‘πΉβπ₯) β β) |
26 | 25 | leidd 11729 |
. . . 4
β’ ((π β β0
β§ π₯ β π) β (β‘πΉβπ₯) β€ (β‘πΉβπ₯)) |
27 | 1, 8, 9, 6, 4 | znleval2 20985 |
. . . . 5
β’ ((π β β0
β§ π₯ β π β§ π₯ β π) β (π₯ β€ π₯ β (β‘πΉβπ₯) β€ (β‘πΉβπ₯))) |
28 | 27 | 3anidm23 1422 |
. . . 4
β’ ((π β β0
β§ π₯ β π) β (π₯ β€ π₯ β (β‘πΉβπ₯) β€ (β‘πΉβπ₯))) |
29 | 26, 28 | mpbird 257 |
. . 3
β’ ((π β β0
β§ π₯ β π) β π₯ β€ π₯) |
30 | 1, 8, 9, 6, 4 | znleval2 20985 |
. . . . . 6
β’ ((π β β0
β§ π₯ β π β§ π¦ β π) β (π₯ β€ π¦ β (β‘πΉβπ₯) β€ (β‘πΉβπ¦))) |
31 | 1, 8, 9, 6, 4 | znleval2 20985 |
. . . . . . 7
β’ ((π β β0
β§ π¦ β π β§ π₯ β π) β (π¦ β€ π₯ β (β‘πΉβπ¦) β€ (β‘πΉβπ₯))) |
32 | 31 | 3com23 1127 |
. . . . . 6
β’ ((π β β0
β§ π₯ β π β§ π¦ β π) β (π¦ β€ π₯ β (β‘πΉβπ¦) β€ (β‘πΉβπ₯))) |
33 | 30, 32 | anbi12d 632 |
. . . . 5
β’ ((π β β0
β§ π₯ β π β§ π¦ β π) β ((π₯ β€ π¦ β§ π¦ β€ π₯) β ((β‘πΉβπ₯) β€ (β‘πΉβπ¦) β§ (β‘πΉβπ¦) β€ (β‘πΉβπ₯)))) |
34 | 25 | 3adant3 1133 |
. . . . . 6
β’ ((π β β0
β§ π₯ β π β§ π¦ β π) β (β‘πΉβπ₯) β β) |
35 | 24 | ffvelcdmda 7039 |
. . . . . . 7
β’ ((π β β0
β§ π¦ β π) β (β‘πΉβπ¦) β β) |
36 | 35 | 3adant2 1132 |
. . . . . 6
β’ ((π β β0
β§ π₯ β π β§ π¦ β π) β (β‘πΉβπ¦) β β) |
37 | 34, 36 | letri3d 11305 |
. . . . 5
β’ ((π β β0
β§ π₯ β π β§ π¦ β π) β ((β‘πΉβπ₯) = (β‘πΉβπ¦) β ((β‘πΉβπ₯) β€ (β‘πΉβπ¦) β§ (β‘πΉβπ¦) β€ (β‘πΉβπ₯)))) |
38 | | f1of1 6787 |
. . . . . . . 8
β’ (β‘πΉ:πβ1-1-ontoβπ β β‘πΉ:πβ1-1βπ) |
39 | 12, 38 | syl 17 |
. . . . . . 7
β’ (π β β0
β β‘πΉ:πβ1-1βπ) |
40 | | f1fveq 7213 |
. . . . . . 7
β’ ((β‘πΉ:πβ1-1βπ β§ (π₯ β π β§ π¦ β π)) β ((β‘πΉβπ₯) = (β‘πΉβπ¦) β π₯ = π¦)) |
41 | 39, 40 | sylan 581 |
. . . . . 6
β’ ((π β β0
β§ (π₯ β π β§ π¦ β π)) β ((β‘πΉβπ₯) = (β‘πΉβπ¦) β π₯ = π¦)) |
42 | 41 | 3impb 1116 |
. . . . 5
β’ ((π β β0
β§ π₯ β π β§ π¦ β π) β ((β‘πΉβπ₯) = (β‘πΉβπ¦) β π₯ = π¦)) |
43 | 33, 37, 42 | 3bitr2d 307 |
. . . 4
β’ ((π β β0
β§ π₯ β π β§ π¦ β π) β ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦)) |
44 | 43 | biimpd 228 |
. . 3
β’ ((π β β0
β§ π₯ β π β§ π¦ β π) β ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦)) |
45 | 25 | 3ad2antr1 1189 |
. . . . 5
β’ ((π β β0
β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (β‘πΉβπ₯) β β) |
46 | 35 | 3ad2antr2 1190 |
. . . . 5
β’ ((π β β0
β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (β‘πΉβπ¦) β β) |
47 | 24 | ffvelcdmda 7039 |
. . . . . 6
β’ ((π β β0
β§ π§ β π) β (β‘πΉβπ§) β β) |
48 | 47 | 3ad2antr3 1191 |
. . . . 5
β’ ((π β β0
β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (β‘πΉβπ§) β β) |
49 | | letr 11257 |
. . . . 5
β’ (((β‘πΉβπ₯) β β β§ (β‘πΉβπ¦) β β β§ (β‘πΉβπ§) β β) β (((β‘πΉβπ₯) β€ (β‘πΉβπ¦) β§ (β‘πΉβπ¦) β€ (β‘πΉβπ§)) β (β‘πΉβπ₯) β€ (β‘πΉβπ§))) |
50 | 45, 46, 48, 49 | syl3anc 1372 |
. . . 4
β’ ((π β β0
β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (((β‘πΉβπ₯) β€ (β‘πΉβπ¦) β§ (β‘πΉβπ¦) β€ (β‘πΉβπ§)) β (β‘πΉβπ₯) β€ (β‘πΉβπ§))) |
51 | 30 | 3adant3r3 1185 |
. . . . 5
β’ ((π β β0
β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯ β€ π¦ β (β‘πΉβπ₯) β€ (β‘πΉβπ¦))) |
52 | 1, 8, 9, 6, 4 | znleval2 20985 |
. . . . . 6
β’ ((π β β0
β§ π¦ β π β§ π§ β π) β (π¦ β€ π§ β (β‘πΉβπ¦) β€ (β‘πΉβπ§))) |
53 | 52 | 3adant3r1 1183 |
. . . . 5
β’ ((π β β0
β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π¦ β€ π§ β (β‘πΉβπ¦) β€ (β‘πΉβπ§))) |
54 | 51, 53 | anbi12d 632 |
. . . 4
β’ ((π β β0
β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯ β€ π¦ β§ π¦ β€ π§) β ((β‘πΉβπ₯) β€ (β‘πΉβπ¦) β§ (β‘πΉβπ¦) β€ (β‘πΉβπ§)))) |
55 | 1, 8, 9, 6, 4 | znleval2 20985 |
. . . . 5
β’ ((π β β0
β§ π₯ β π β§ π§ β π) β (π₯ β€ π§ β (β‘πΉβπ₯) β€ (β‘πΉβπ§))) |
56 | 55 | 3adant3r2 1184 |
. . . 4
β’ ((π β β0
β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯ β€ π§ β (β‘πΉβπ₯) β€ (β‘πΉβπ§))) |
57 | 50, 54, 56 | 3imtr4d 294 |
. . 3
β’ ((π β β0
β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)) |
58 | 3, 5, 7, 29, 44, 57 | isposd 18220 |
. 2
β’ (π β β0
β π β
Poset) |
59 | 34, 36 | letrid 11315 |
. . . . 5
β’ ((π β β0
β§ π₯ β π β§ π¦ β π) β ((β‘πΉβπ₯) β€ (β‘πΉβπ¦) β¨ (β‘πΉβπ¦) β€ (β‘πΉβπ₯))) |
60 | 30, 32 | orbi12d 918 |
. . . . 5
β’ ((π β β0
β§ π₯ β π β§ π¦ β π) β ((π₯ β€ π¦ β¨ π¦ β€ π₯) β ((β‘πΉβπ₯) β€ (β‘πΉβπ¦) β¨ (β‘πΉβπ¦) β€ (β‘πΉβπ₯)))) |
61 | 59, 60 | mpbird 257 |
. . . 4
β’ ((π β β0
β§ π₯ β π β§ π¦ β π) β (π₯ β€ π¦ β¨ π¦ β€ π₯)) |
62 | 61 | 3expb 1121 |
. . 3
β’ ((π β β0
β§ (π₯ β π β§ π¦ β π)) β (π₯ β€ π¦ β¨ π¦ β€ π₯)) |
63 | 62 | ralrimivva 3194 |
. 2
β’ (π β β0
β βπ₯ β
π βπ¦ β π (π₯ β€ π¦ β¨ π¦ β€ π₯)) |
64 | 4, 6 | istos 18315 |
. 2
β’ (π β Toset β (π β Poset β§
βπ₯ β π βπ¦ β π (π₯ β€ π¦ β¨ π¦ β€ π₯))) |
65 | 58, 63, 64 | sylanbrc 584 |
1
β’ (π β β0
β π β
Toset) |