Step | Hyp | Ref
| Expression |
1 | | elfznn 13532 |
. . . . 5
β’ (π΄ β (1...π) β π΄ β β) |
2 | 1 | adantl 482 |
. . . 4
β’ ((π β§ π΄ β (1...π)) β π΄ β β) |
3 | | elfz1end 13533 |
. . . 4
β’ (π΄ β β β π΄ β (1...π΄)) |
4 | 2, 3 | sylib 217 |
. . 3
β’ ((π β§ π΄ β (1...π)) β π΄ β (1...π΄)) |
5 | 4 | snssd 4812 |
. 2
β’ ((π β§ π΄ β (1...π)) β {π΄} β (1...π΄)) |
6 | | elsni 4645 |
. . . . . . 7
β’ (π₯ β {π΄} β π₯ = π΄) |
7 | | elsni 4645 |
. . . . . . 7
β’ (π¦ β {π΄} β π¦ = π΄) |
8 | 6, 7 | breqan12d 5164 |
. . . . . 6
β’ ((π₯ β {π΄} β§ π¦ β {π΄}) β (π₯ < π¦ β π΄ < π΄)) |
9 | 8 | adantl 482 |
. . . . 5
β’ (((π β§ π΄ β (1...π)) β§ (π₯ β {π΄} β§ π¦ β {π΄})) β (π₯ < π¦ β π΄ < π΄)) |
10 | | fzssuz 13544 |
. . . . . . . . 9
β’
(1...π) β
(β€β₯β1) |
11 | | uzssz 12845 |
. . . . . . . . . 10
β’
(β€β₯β1) β β€ |
12 | | zssre 12567 |
. . . . . . . . . 10
β’ β€
β β |
13 | 11, 12 | sstri 3991 |
. . . . . . . . 9
β’
(β€β₯β1) β β |
14 | 10, 13 | sstri 3991 |
. . . . . . . 8
β’
(1...π) β
β |
15 | | simpr 485 |
. . . . . . . . 9
β’ ((π β§ π΄ β (1...π)) β π΄ β (1...π)) |
16 | 15 | adantr 481 |
. . . . . . . 8
β’ (((π β§ π΄ β (1...π)) β§ (π₯ β {π΄} β§ π¦ β {π΄})) β π΄ β (1...π)) |
17 | 14, 16 | sselid 3980 |
. . . . . . 7
β’ (((π β§ π΄ β (1...π)) β§ (π₯ β {π΄} β§ π¦ β {π΄})) β π΄ β β) |
18 | 17 | ltnrd 11350 |
. . . . . 6
β’ (((π β§ π΄ β (1...π)) β§ (π₯ β {π΄} β§ π¦ β {π΄})) β Β¬ π΄ < π΄) |
19 | 18 | pm2.21d 121 |
. . . . 5
β’ (((π β§ π΄ β (1...π)) β§ (π₯ β {π΄} β§ π¦ β {π΄})) β (π΄ < π΄ β (πΉβπ₯)π(πΉβπ¦))) |
20 | 9, 19 | sylbid 239 |
. . . 4
β’ (((π β§ π΄ β (1...π)) β§ (π₯ β {π΄} β§ π¦ β {π΄})) β (π₯ < π¦ β (πΉβπ₯)π(πΉβπ¦))) |
21 | 20 | ralrimivva 3200 |
. . 3
β’ ((π β§ π΄ β (1...π)) β βπ₯ β {π΄}βπ¦ β {π΄} (π₯ < π¦ β (πΉβπ₯)π(πΉβπ¦))) |
22 | | erdsze.f |
. . . . . 6
β’ (π β πΉ:(1...π)β1-1ββ) |
23 | | f1f 6787 |
. . . . . 6
β’ (πΉ:(1...π)β1-1ββ β πΉ:(1...π)βΆβ) |
24 | 22, 23 | syl 17 |
. . . . 5
β’ (π β πΉ:(1...π)βΆβ) |
25 | 24 | adantr 481 |
. . . 4
β’ ((π β§ π΄ β (1...π)) β πΉ:(1...π)βΆβ) |
26 | 15 | snssd 4812 |
. . . 4
β’ ((π β§ π΄ β (1...π)) β {π΄} β (1...π)) |
27 | | ltso 11296 |
. . . . . 6
β’ < Or
β |
28 | | soss 5608 |
. . . . . 6
β’
((1...π) β
β β ( < Or β β < Or (1...π))) |
29 | 14, 27, 28 | mp2 9 |
. . . . 5
β’ < Or
(1...π) |
30 | | erdszelem.o |
. . . . 5
β’ π Or β |
31 | | soisores 7326 |
. . . . 5
β’ ((( <
Or (1...π) β§ π Or β) β§ (πΉ:(1...π)βΆβ β§ {π΄} β (1...π))) β ((πΉ βΎ {π΄}) Isom < , π ({π΄}, (πΉ β {π΄})) β βπ₯ β {π΄}βπ¦ β {π΄} (π₯ < π¦ β (πΉβπ₯)π(πΉβπ¦)))) |
32 | 29, 30, 31 | mpanl12 700 |
. . . 4
β’ ((πΉ:(1...π)βΆβ β§ {π΄} β (1...π)) β ((πΉ βΎ {π΄}) Isom < , π ({π΄}, (πΉ β {π΄})) β βπ₯ β {π΄}βπ¦ β {π΄} (π₯ < π¦ β (πΉβπ₯)π(πΉβπ¦)))) |
33 | 25, 26, 32 | syl2anc 584 |
. . 3
β’ ((π β§ π΄ β (1...π)) β ((πΉ βΎ {π΄}) Isom < , π ({π΄}, (πΉ β {π΄})) β βπ₯ β {π΄}βπ¦ β {π΄} (π₯ < π¦ β (πΉβπ₯)π(πΉβπ¦)))) |
34 | 21, 33 | mpbird 256 |
. 2
β’ ((π β§ π΄ β (1...π)) β (πΉ βΎ {π΄}) Isom < , π ({π΄}, (πΉ β {π΄}))) |
35 | | snidg 4662 |
. . 3
β’ (π΄ β (1...π) β π΄ β {π΄}) |
36 | 35 | adantl 482 |
. 2
β’ ((π β§ π΄ β (1...π)) β π΄ β {π΄}) |
37 | | eqid 2732 |
. . 3
β’ {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)} = {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)} |
38 | 37 | erdszelem1 34251 |
. 2
β’ ({π΄} β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)} β ({π΄} β (1...π΄) β§ (πΉ βΎ {π΄}) Isom < , π ({π΄}, (πΉ β {π΄})) β§ π΄ β {π΄})) |
39 | 5, 34, 36, 38 | syl3anbrc 1343 |
1
β’ ((π β§ π΄ β (1...π)) β {π΄} β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)}) |