Step | Hyp | Ref
| Expression |
1 | | cvrletr.b |
. . 3
β’ π΅ = (BaseβπΎ) |
2 | | cvrletr.s |
. . 3
β’ < =
(ltβπΎ) |
3 | | cvrletr.c |
. . 3
β’ πΆ = ( β βπΎ) |
4 | 1, 2, 3 | cvrval 37777 |
. 2
β’ ((πΎ β π΄ β§ π β π΅ β§ π β π΅) β (ππΆπ β (π < π β§ Β¬ βπ§ β π΅ (π < π§ β§ π§ < π)))) |
5 | | iman 403 |
. . . . . . . 8
β’ (((π < π§ β§ π§ β€ π) β π§ = π) β Β¬ ((π < π§ β§ π§ β€ π) β§ Β¬ π§ = π)) |
6 | | df-ne 2941 |
. . . . . . . . 9
β’ (π§ β π β Β¬ π§ = π) |
7 | 6 | anbi2i 624 |
. . . . . . . 8
β’ (((π < π§ β§ π§ β€ π) β§ π§ β π) β ((π < π§ β§ π§ β€ π) β§ Β¬ π§ = π)) |
8 | 5, 7 | xchbinxr 335 |
. . . . . . 7
β’ (((π < π§ β§ π§ β€ π) β π§ = π) β Β¬ ((π < π§ β§ π§ β€ π) β§ π§ β π)) |
9 | | anass 470 |
. . . . . . . . 9
β’ (((π < π§ β§ π§ β€ π) β§ π§ β π) β (π < π§ β§ (π§ β€ π β§ π§ β π))) |
10 | | cvrletr.l |
. . . . . . . . . . . . 13
β’ β€ =
(leβπΎ) |
11 | 10, 2 | pltval 18226 |
. . . . . . . . . . . 12
β’ ((πΎ β π΄ β§ π§ β π΅ β§ π β π΅) β (π§ < π β (π§ β€ π β§ π§ β π))) |
12 | 11 | 3com23 1127 |
. . . . . . . . . . 11
β’ ((πΎ β π΄ β§ π β π΅ β§ π§ β π΅) β (π§ < π β (π§ β€ π β§ π§ β π))) |
13 | 12 | 3expa 1119 |
. . . . . . . . . 10
β’ (((πΎ β π΄ β§ π β π΅) β§ π§ β π΅) β (π§ < π β (π§ β€ π β§ π§ β π))) |
14 | 13 | anbi2d 630 |
. . . . . . . . 9
β’ (((πΎ β π΄ β§ π β π΅) β§ π§ β π΅) β ((π < π§ β§ π§ < π) β (π < π§ β§ (π§ β€ π β§ π§ β π)))) |
15 | 9, 14 | bitr4id 290 |
. . . . . . . 8
β’ (((πΎ β π΄ β§ π β π΅) β§ π§ β π΅) β (((π < π§ β§ π§ β€ π) β§ π§ β π) β (π < π§ β§ π§ < π))) |
16 | 15 | notbid 318 |
. . . . . . 7
β’ (((πΎ β π΄ β§ π β π΅) β§ π§ β π΅) β (Β¬ ((π < π§ β§ π§ β€ π) β§ π§ β π) β Β¬ (π < π§ β§ π§ < π))) |
17 | 8, 16 | bitrid 283 |
. . . . . 6
β’ (((πΎ β π΄ β§ π β π΅) β§ π§ β π΅) β (((π < π§ β§ π§ β€ π) β π§ = π) β Β¬ (π < π§ β§ π§ < π))) |
18 | 17 | ralbidva 3169 |
. . . . 5
β’ ((πΎ β π΄ β§ π β π΅) β (βπ§ β π΅ ((π < π§ β§ π§ β€ π) β π§ = π) β βπ§ β π΅ Β¬ (π < π§ β§ π§ < π))) |
19 | | ralnex 3072 |
. . . . 5
β’
(βπ§ β
π΅ Β¬ (π < π§ β§ π§ < π) β Β¬ βπ§ β π΅ (π < π§ β§ π§ < π)) |
20 | 18, 19 | bitrdi 287 |
. . . 4
β’ ((πΎ β π΄ β§ π β π΅) β (βπ§ β π΅ ((π < π§ β§ π§ β€ π) β π§ = π) β Β¬ βπ§ β π΅ (π < π§ β§ π§ < π))) |
21 | 20 | anbi2d 630 |
. . 3
β’ ((πΎ β π΄ β§ π β π΅) β ((π < π β§ βπ§ β π΅ ((π < π§ β§ π§ β€ π) β π§ = π)) β (π < π β§ Β¬ βπ§ β π΅ (π < π§ β§ π§ < π)))) |
22 | 21 | 3adant2 1132 |
. 2
β’ ((πΎ β π΄ β§ π β π΅ β§ π β π΅) β ((π < π β§ βπ§ β π΅ ((π < π§ β§ π§ β€ π) β π§ = π)) β (π < π β§ Β¬ βπ§ β π΅ (π < π§ β§ π§ < π)))) |
23 | 4, 22 | bitr4d 282 |
1
β’ ((πΎ β π΄ β§ π β π΅ β§ π β π΅) β (ππΆπ β (π < π β§ βπ§ β π΅ ((π < π§ β§ π§ β€ π) β π§ = π)))) |