Step | Hyp | Ref
| Expression |
1 | | isarchi2.b |
. . . 4
β’ π΅ = (Baseβπ) |
2 | | isarchi2.0 |
. . . 4
β’ 0 =
(0gβπ) |
3 | | eqid 2733 |
. . . 4
β’
(ββπ) =
(ββπ) |
4 | 1, 2, 3 | isarchi 32328 |
. . 3
β’ (π β Toset β (π β Archi β
βπ₯ β π΅ βπ¦ β π΅ Β¬ π₯(ββπ)π¦)) |
5 | 4 | adantr 482 |
. 2
β’ ((π β Toset β§ π β Mnd) β (π β Archi β
βπ₯ β π΅ βπ¦ β π΅ Β¬ π₯(ββπ)π¦)) |
6 | | simpl1l 1225 |
. . . . . . . 8
β’ ((((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β§ π β β) β π β Toset) |
7 | | isarchi2.x |
. . . . . . . . 9
β’ Β· =
(.gβπ) |
8 | | simpl1r 1226 |
. . . . . . . . 9
β’ ((((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β§ π β β) β π β Mnd) |
9 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β§ π β β) β π β β) |
10 | 9 | nnnn0d 12532 |
. . . . . . . . 9
β’ ((((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β§ π β β) β π β β0) |
11 | | simpl2 1193 |
. . . . . . . . 9
β’ ((((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β§ π β β) β π₯ β π΅) |
12 | 1, 7, 8, 10, 11 | mulgnn0cld 18975 |
. . . . . . . 8
β’ ((((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β§ π β β) β (π Β· π₯) β π΅) |
13 | | simpl3 1194 |
. . . . . . . 8
β’ ((((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β§ π β β) β π¦ β π΅) |
14 | | isarchi2.l |
. . . . . . . . . 10
β’ β€ =
(leβπ) |
15 | | isarchi2.t |
. . . . . . . . . 10
β’ < =
(ltβπ) |
16 | 1, 14, 15 | tltnle 18375 |
. . . . . . . . 9
β’ ((π β Toset β§ (π Β· π₯) β π΅ β§ π¦ β π΅) β ((π Β· π₯) < π¦ β Β¬ π¦ β€ (π Β· π₯))) |
17 | 16 | con2bid 355 |
. . . . . . . 8
β’ ((π β Toset β§ (π Β· π₯) β π΅ β§ π¦ β π΅) β (π¦ β€ (π Β· π₯) β Β¬ (π Β· π₯) < π¦)) |
18 | 6, 12, 13, 17 | syl3anc 1372 |
. . . . . . 7
β’ ((((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β§ π β β) β (π¦ β€ (π Β· π₯) β Β¬ (π Β· π₯) < π¦)) |
19 | 18 | rexbidva 3177 |
. . . . . 6
β’ (((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β (βπ β β π¦ β€ (π Β· π₯) β βπ β β Β¬ (π Β· π₯) < π¦)) |
20 | 19 | imbi2d 341 |
. . . . 5
β’ (((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β (( 0 < π₯ β βπ β β π¦ β€ (π Β· π₯)) β ( 0 < π₯ β βπ β β Β¬ (π Β· π₯) < π¦))) |
21 | 1, 2, 7, 15 | isinftm 32327 |
. . . . . . . 8
β’ ((π β Toset β§ π₯ β π΅ β§ π¦ β π΅) β (π₯(ββπ)π¦ β ( 0 < π₯ β§ βπ β β (π Β· π₯) < π¦))) |
22 | 21 | notbid 318 |
. . . . . . 7
β’ ((π β Toset β§ π₯ β π΅ β§ π¦ β π΅) β (Β¬ π₯(ββπ)π¦ β Β¬ ( 0 < π₯ β§ βπ β β (π Β· π₯) < π¦))) |
23 | | rexnal 3101 |
. . . . . . . . 9
β’
(βπ β
β Β¬ (π Β· π₯) < π¦ β Β¬ βπ β β (π Β· π₯) < π¦) |
24 | 23 | imbi2i 336 |
. . . . . . . 8
β’ (( 0 < π₯ β βπ β β Β¬ (π Β· π₯) < π¦) β ( 0 < π₯ β Β¬ βπ β β (π Β· π₯) < π¦)) |
25 | | imnan 401 |
. . . . . . . 8
β’ (( 0 < π₯ β Β¬ βπ β β (π Β· π₯) < π¦) β Β¬ ( 0 < π₯ β§ βπ β β (π Β· π₯) < π¦)) |
26 | 24, 25 | bitr2i 276 |
. . . . . . 7
β’ (Β¬ (
0 < π₯ β§ βπ β β (π Β· π₯) < π¦) β ( 0 < π₯ β βπ β β Β¬ (π Β· π₯) < π¦)) |
27 | 22, 26 | bitrdi 287 |
. . . . . 6
β’ ((π β Toset β§ π₯ β π΅ β§ π¦ β π΅) β (Β¬ π₯(ββπ)π¦ β ( 0 < π₯ β βπ β β Β¬ (π Β· π₯) < π¦))) |
28 | 27 | 3adant1r 1178 |
. . . . 5
β’ (((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β (Β¬ π₯(ββπ)π¦ β ( 0 < π₯ β βπ β β Β¬ (π Β· π₯) < π¦))) |
29 | 20, 28 | bitr4d 282 |
. . . 4
β’ (((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β (( 0 < π₯ β βπ β β π¦ β€ (π Β· π₯)) β Β¬ π₯(ββπ)π¦)) |
30 | 29 | 3expb 1121 |
. . 3
β’ (((π β Toset β§ π β Mnd) β§ (π₯ β π΅ β§ π¦ β π΅)) β (( 0 < π₯ β βπ β β π¦ β€ (π Β· π₯)) β Β¬ π₯(ββπ)π¦)) |
31 | 30 | 2ralbidva 3217 |
. 2
β’ ((π β Toset β§ π β Mnd) β
(βπ₯ β π΅ βπ¦ β π΅ ( 0 < π₯ β βπ β β π¦ β€ (π Β· π₯)) β βπ₯ β π΅ βπ¦ β π΅ Β¬ π₯(ββπ)π¦)) |
32 | 5, 31 | bitr4d 282 |
1
β’ ((π β Toset β§ π β Mnd) β (π β Archi β
βπ₯ β π΅ βπ¦ β π΅ ( 0 < π₯ β βπ β β π¦ β€ (π Β· π₯)))) |