Step | Hyp | Ref
| Expression |
1 | | isarchi2.b |
. . . 4
β’ π΅ = (Baseβπ) |
2 | | isarchi2.0 |
. . . 4
β’ 0 =
(0gβπ) |
3 | | eqid 2731 |
. . . 4
β’
(ββπ) =
(ββπ) |
4 | 1, 2, 3 | isarchi 32595 |
. . 3
β’ (π β Toset β (π β Archi β
βπ₯ β π΅ βπ¦ β π΅ Β¬ π₯(ββπ)π¦)) |
5 | 4 | adantr 480 |
. 2
β’ ((π β Toset β§ π β Mnd) β (π β Archi β
βπ₯ β π΅ βπ¦ β π΅ Β¬ π₯(ββπ)π¦)) |
6 | | simpl1l 1223 |
. . . . . . . 8
β’ ((((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β§ π β β) β π β Toset) |
7 | | isarchi2.x |
. . . . . . . . 9
β’ Β· =
(.gβπ) |
8 | | simpl1r 1224 |
. . . . . . . . 9
β’ ((((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β§ π β β) β π β Mnd) |
9 | | simpr 484 |
. . . . . . . . . 10
β’ ((((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β§ π β β) β π β β) |
10 | 9 | nnnn0d 12537 |
. . . . . . . . 9
β’ ((((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β§ π β β) β π β β0) |
11 | | simpl2 1191 |
. . . . . . . . 9
β’ ((((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β§ π β β) β π₯ β π΅) |
12 | 1, 7, 8, 10, 11 | mulgnn0cld 19012 |
. . . . . . . 8
β’ ((((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β§ π β β) β (π Β· π₯) β π΅) |
13 | | simpl3 1192 |
. . . . . . . 8
β’ ((((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β§ π β β) β π¦ β π΅) |
14 | | isarchi2.l |
. . . . . . . . . 10
β’ β€ =
(leβπ) |
15 | | isarchi2.t |
. . . . . . . . . 10
β’ < =
(ltβπ) |
16 | 1, 14, 15 | tltnle 18380 |
. . . . . . . . 9
β’ ((π β Toset β§ (π Β· π₯) β π΅ β§ π¦ β π΅) β ((π Β· π₯) < π¦ β Β¬ π¦ β€ (π Β· π₯))) |
17 | 16 | con2bid 353 |
. . . . . . . 8
β’ ((π β Toset β§ (π Β· π₯) β π΅ β§ π¦ β π΅) β (π¦ β€ (π Β· π₯) β Β¬ (π Β· π₯) < π¦)) |
18 | 6, 12, 13, 17 | syl3anc 1370 |
. . . . . . 7
β’ ((((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β§ π β β) β (π¦ β€ (π Β· π₯) β Β¬ (π Β· π₯) < π¦)) |
19 | 18 | rexbidva 3175 |
. . . . . 6
β’ (((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β (βπ β β π¦ β€ (π Β· π₯) β βπ β β Β¬ (π Β· π₯) < π¦)) |
20 | 19 | imbi2d 339 |
. . . . 5
β’ (((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β (( 0 < π₯ β βπ β β π¦ β€ (π Β· π₯)) β ( 0 < π₯ β βπ β β Β¬ (π Β· π₯) < π¦))) |
21 | 1, 2, 7, 15 | isinftm 32594 |
. . . . . . . 8
β’ ((π β Toset β§ π₯ β π΅ β§ π¦ β π΅) β (π₯(ββπ)π¦ β ( 0 < π₯ β§ βπ β β (π Β· π₯) < π¦))) |
22 | 21 | notbid 317 |
. . . . . . 7
β’ ((π β Toset β§ π₯ β π΅ β§ π¦ β π΅) β (Β¬ π₯(ββπ)π¦ β Β¬ ( 0 < π₯ β§ βπ β β (π Β· π₯) < π¦))) |
23 | | rexnal 3099 |
. . . . . . . . 9
β’
(βπ β
β Β¬ (π Β· π₯) < π¦ β Β¬ βπ β β (π Β· π₯) < π¦) |
24 | 23 | imbi2i 335 |
. . . . . . . 8
β’ (( 0 < π₯ β βπ β β Β¬ (π Β· π₯) < π¦) β ( 0 < π₯ β Β¬ βπ β β (π Β· π₯) < π¦)) |
25 | | imnan 399 |
. . . . . . . 8
β’ (( 0 < π₯ β Β¬ βπ β β (π Β· π₯) < π¦) β Β¬ ( 0 < π₯ β§ βπ β β (π Β· π₯) < π¦)) |
26 | 24, 25 | bitr2i 275 |
. . . . . . 7
β’ (Β¬ (
0 < π₯ β§ βπ β β (π Β· π₯) < π¦) β ( 0 < π₯ β βπ β β Β¬ (π Β· π₯) < π¦)) |
27 | 22, 26 | bitrdi 286 |
. . . . . 6
β’ ((π β Toset β§ π₯ β π΅ β§ π¦ β π΅) β (Β¬ π₯(ββπ)π¦ β ( 0 < π₯ β βπ β β Β¬ (π Β· π₯) < π¦))) |
28 | 27 | 3adant1r 1176 |
. . . . 5
β’ (((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β (Β¬ π₯(ββπ)π¦ β ( 0 < π₯ β βπ β β Β¬ (π Β· π₯) < π¦))) |
29 | 20, 28 | bitr4d 281 |
. . . 4
β’ (((π β Toset β§ π β Mnd) β§ π₯ β π΅ β§ π¦ β π΅) β (( 0 < π₯ β βπ β β π¦ β€ (π Β· π₯)) β Β¬ π₯(ββπ)π¦)) |
30 | 29 | 3expb 1119 |
. . 3
β’ (((π β Toset β§ π β Mnd) β§ (π₯ β π΅ β§ π¦ β π΅)) β (( 0 < π₯ β βπ β β π¦ β€ (π Β· π₯)) β Β¬ π₯(ββπ)π¦)) |
31 | 30 | 2ralbidva 3215 |
. 2
β’ ((π β Toset β§ π β Mnd) β
(βπ₯ β π΅ βπ¦ β π΅ ( 0 < π₯ β βπ β β π¦ β€ (π Β· π₯)) β βπ₯ β π΅ βπ¦ β π΅ Β¬ π₯(ββπ)π¦)) |
32 | 5, 31 | bitr4d 281 |
1
β’ ((π β Toset β§ π β Mnd) β (π β Archi β
βπ₯ β π΅ βπ¦ β π΅ ( 0 < π₯ β βπ β β π¦ β€ (π Β· π₯)))) |