Step | Hyp | Ref
| Expression |
1 | | dvgt0lem.i |
. . . . . 6
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (πΉβπ₯)π(πΉβπ¦)) |
2 | 1 | ex 412 |
. . . . 5
β’ ((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β (π₯ < π¦ β (πΉβπ₯)π(πΉβπ¦))) |
3 | 2 | ralrimivva 3194 |
. . . 4
β’ (π β βπ₯ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)(π₯ < π¦ β (πΉβπ₯)π(πΉβπ¦))) |
4 | | dvgt0.a |
. . . . . . 7
β’ (π β π΄ β β) |
5 | | dvgt0.b |
. . . . . . 7
β’ (π β π΅ β β) |
6 | | iccssre 13412 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
7 | 4, 5, 6 | syl2anc 583 |
. . . . . 6
β’ (π β (π΄[,]π΅) β β) |
8 | | ltso 11298 |
. . . . . 6
β’ < Or
β |
9 | | soss 5601 |
. . . . . 6
β’ ((π΄[,]π΅) β β β ( < Or β
β < Or (π΄[,]π΅))) |
10 | 7, 8, 9 | mpisyl 21 |
. . . . 5
β’ (π β < Or (π΄[,]π΅)) |
11 | | dvgt0lem.o |
. . . . . 6
β’ π Or β |
12 | 11 | a1i 11 |
. . . . 5
β’ (π β π Or β) |
13 | | dvgt0.f |
. . . . . 6
β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) |
14 | | cncff 24768 |
. . . . . 6
β’ (πΉ β ((π΄[,]π΅)βcnββ) β πΉ:(π΄[,]π΅)βΆβ) |
15 | 13, 14 | syl 17 |
. . . . 5
β’ (π β πΉ:(π΄[,]π΅)βΆβ) |
16 | | ssidd 4000 |
. . . . 5
β’ (π β (π΄[,]π΅) β (π΄[,]π΅)) |
17 | | soisores 7320 |
. . . . 5
β’ ((( <
Or (π΄[,]π΅) β§ π Or β) β§ (πΉ:(π΄[,]π΅)βΆβ β§ (π΄[,]π΅) β (π΄[,]π΅))) β ((πΉ βΎ (π΄[,]π΅)) Isom < , π ((π΄[,]π΅), (πΉ β (π΄[,]π΅))) β βπ₯ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)(π₯ < π¦ β (πΉβπ₯)π(πΉβπ¦)))) |
18 | 10, 12, 15, 16, 17 | syl22anc 836 |
. . . 4
β’ (π β ((πΉ βΎ (π΄[,]π΅)) Isom < , π ((π΄[,]π΅), (πΉ β (π΄[,]π΅))) β βπ₯ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)(π₯ < π¦ β (πΉβπ₯)π(πΉβπ¦)))) |
19 | 3, 18 | mpbird 257 |
. . 3
β’ (π β (πΉ βΎ (π΄[,]π΅)) Isom < , π ((π΄[,]π΅), (πΉ β (π΄[,]π΅)))) |
20 | | ffn 6711 |
. . . . 5
β’ (πΉ:(π΄[,]π΅)βΆβ β πΉ Fn (π΄[,]π΅)) |
21 | 13, 14, 20 | 3syl 18 |
. . . 4
β’ (π β πΉ Fn (π΄[,]π΅)) |
22 | | fnresdm 6663 |
. . . 4
β’ (πΉ Fn (π΄[,]π΅) β (πΉ βΎ (π΄[,]π΅)) = πΉ) |
23 | | isoeq1 7310 |
. . . 4
β’ ((πΉ βΎ (π΄[,]π΅)) = πΉ β ((πΉ βΎ (π΄[,]π΅)) Isom < , π ((π΄[,]π΅), (πΉ β (π΄[,]π΅))) β πΉ Isom < , π ((π΄[,]π΅), (πΉ β (π΄[,]π΅))))) |
24 | 21, 22, 23 | 3syl 18 |
. . 3
β’ (π β ((πΉ βΎ (π΄[,]π΅)) Isom < , π ((π΄[,]π΅), (πΉ β (π΄[,]π΅))) β πΉ Isom < , π ((π΄[,]π΅), (πΉ β (π΄[,]π΅))))) |
25 | 19, 24 | mpbid 231 |
. 2
β’ (π β πΉ Isom < , π ((π΄[,]π΅), (πΉ β (π΄[,]π΅)))) |
26 | | fnima 6674 |
. . 3
β’ (πΉ Fn (π΄[,]π΅) β (πΉ β (π΄[,]π΅)) = ran πΉ) |
27 | | isoeq5 7314 |
. . 3
β’ ((πΉ β (π΄[,]π΅)) = ran πΉ β (πΉ Isom < , π ((π΄[,]π΅), (πΉ β (π΄[,]π΅))) β πΉ Isom < , π ((π΄[,]π΅), ran πΉ))) |
28 | 21, 26, 27 | 3syl 18 |
. 2
β’ (π β (πΉ Isom < , π ((π΄[,]π΅), (πΉ β (π΄[,]π΅))) β πΉ Isom < , π ((π΄[,]π΅), ran πΉ))) |
29 | 25, 28 | mpbid 231 |
1
β’ (π β πΉ Isom < , π ((π΄[,]π΅), ran πΉ)) |