Step | Hyp | Ref
| Expression |
1 | | tosglb.1 |
. . . . . . 7
β’ (π β πΎ β Toset) |
2 | 1 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β π΅) β§ π β π΄) β πΎ β Toset) |
3 | | tosglb.2 |
. . . . . . . 8
β’ (π β π΄ β π΅) |
4 | 3 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π΅) β π΄ β π΅) |
5 | 4 | sselda 3945 |
. . . . . 6
β’ (((π β§ π β π΅) β§ π β π΄) β π β π΅) |
6 | | simplr 768 |
. . . . . 6
β’ (((π β§ π β π΅) β§ π β π΄) β π β π΅) |
7 | | tosglb.b |
. . . . . . 7
β’ π΅ = (BaseβπΎ) |
8 | | tosglb.e |
. . . . . . 7
β’ β€ =
(leβπΎ) |
9 | | tosglb.l |
. . . . . . 7
β’ < =
(ltβπΎ) |
10 | 7, 8, 9 | tltnle 18316 |
. . . . . 6
β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π < π β Β¬ π β€ π)) |
11 | 2, 5, 6, 10 | syl3anc 1372 |
. . . . 5
β’ (((π β§ π β π΅) β§ π β π΄) β (π < π β Β¬ π β€ π)) |
12 | 11 | con2bid 355 |
. . . 4
β’ (((π β§ π β π΅) β§ π β π΄) β (π β€ π β Β¬ π < π)) |
13 | 12 | ralbidva 3169 |
. . 3
β’ ((π β§ π β π΅) β (βπ β π΄ π β€ π β βπ β π΄ Β¬ π < π)) |
14 | 3 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΅) β§ π β π΄) β π΄ β π΅) |
15 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΅) β§ π β π΄) β π β π΄) |
16 | 14, 15 | sseldd 3946 |
. . . . . . . . . . 11
β’ (((π β§ π β π΅) β§ π β π΄) β π β π΅) |
17 | 7, 8, 9 | tltnle 18316 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π < π β Β¬ π β€ π)) |
18 | 1, 17 | syl3an1 1164 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΅ β§ π β π΅) β (π < π β Β¬ π β€ π)) |
19 | 18 | 3com23 1127 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅ β§ π β π΅) β (π < π β Β¬ π β€ π)) |
20 | 19 | 3expa 1119 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΅) β§ π β π΅) β (π < π β Β¬ π β€ π)) |
21 | 20 | con2bid 355 |
. . . . . . . . . . 11
β’ (((π β§ π β π΅) β§ π β π΅) β (π β€ π β Β¬ π < π)) |
22 | 16, 21 | syldan 592 |
. . . . . . . . . 10
β’ (((π β§ π β π΅) β§ π β π΄) β (π β€ π β Β¬ π < π)) |
23 | 22 | ralbidva 3169 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β (βπ β π΄ π β€ π β βπ β π΄ Β¬ π < π)) |
24 | | breq1 5109 |
. . . . . . . . . . . 12
β’ (π = π β (π < π β π < π)) |
25 | 24 | notbid 318 |
. . . . . . . . . . 11
β’ (π = π β (Β¬ π < π β Β¬ π < π)) |
26 | 25 | cbvralvw 3224 |
. . . . . . . . . 10
β’
(βπ β
π΄ Β¬ π < π β βπ β π΄ Β¬ π < π) |
27 | | ralnex 3072 |
. . . . . . . . . 10
β’
(βπ β
π΄ Β¬ π < π β Β¬ βπ β π΄ π < π) |
28 | 26, 27 | bitri 275 |
. . . . . . . . 9
β’
(βπ β
π΄ Β¬ π < π β Β¬ βπ β π΄ π < π) |
29 | 23, 28 | bitrdi 287 |
. . . . . . . 8
β’ ((π β§ π β π΅) β (βπ β π΄ π β€ π β Β¬ βπ β π΄ π < π)) |
30 | 29 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π β π΅) β§ π β π΅) β (βπ β π΄ π β€ π β Β¬ βπ β π΄ π < π)) |
31 | 1 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β π΅) β§ π β π΅) β πΎ β Toset) |
32 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ π β π΅) β§ π β π΅) β π β π΅) |
33 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π β π΅) β§ π β π΅) β π β π΅) |
34 | 7, 8, 9 | tltnle 18316 |
. . . . . . . . 9
β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π < π β Β¬ π β€ π)) |
35 | 31, 32, 33, 34 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ π β π΅) β§ π β π΅) β (π < π β Β¬ π β€ π)) |
36 | 35 | con2bid 355 |
. . . . . . 7
β’ (((π β§ π β π΅) β§ π β π΅) β (π β€ π β Β¬ π < π)) |
37 | 30, 36 | imbi12d 345 |
. . . . . 6
β’ (((π β§ π β π΅) β§ π β π΅) β ((βπ β π΄ π β€ π β π β€ π) β (Β¬ βπ β π΄ π < π β Β¬ π < π))) |
38 | | con34b 316 |
. . . . . 6
β’ ((π < π β βπ β π΄ π < π) β (Β¬ βπ β π΄ π < π β Β¬ π < π)) |
39 | 37, 38 | bitr4di 289 |
. . . . 5
β’ (((π β§ π β π΅) β§ π β π΅) β ((βπ β π΄ π β€ π β π β€ π) β (π < π β βπ β π΄ π < π))) |
40 | 39 | ralbidva 3169 |
. . . 4
β’ ((π β§ π β π΅) β (βπ β π΅ (βπ β π΄ π β€ π β π β€ π) β βπ β π΅ (π < π β βπ β π΄ π < π))) |
41 | | breq2 5110 |
. . . . . 6
β’ (π = π β (π < π β π < π)) |
42 | | breq2 5110 |
. . . . . . 7
β’ (π = π β (π < π β π < π)) |
43 | 42 | rexbidv 3172 |
. . . . . 6
β’ (π = π β (βπ β π΄ π < π β βπ β π΄ π < π)) |
44 | 41, 43 | imbi12d 345 |
. . . . 5
β’ (π = π β ((π < π β βπ β π΄ π < π) β (π < π β βπ β π΄ π < π))) |
45 | 44 | cbvralvw 3224 |
. . . 4
β’
(βπ β
π΅ (π < π β βπ β π΄ π < π) β βπ β π΅ (π < π β βπ β π΄ π < π)) |
46 | 40, 45 | bitr4di 289 |
. . 3
β’ ((π β§ π β π΅) β (βπ β π΅ (βπ β π΄ π β€ π β π β€ π) β βπ β π΅ (π < π β βπ β π΄ π < π))) |
47 | 13, 46 | anbi12d 632 |
. 2
β’ ((π β§ π β π΅) β ((βπ β π΄ π β€ π β§ βπ β π΅ (βπ β π΄ π β€ π β π β€ π)) β (βπ β π΄ Β¬ π < π β§ βπ β π΅ (π < π β βπ β π΄ π < π)))) |
48 | | vex 3448 |
. . . . . 6
β’ π β V |
49 | | vex 3448 |
. . . . . 6
β’ π β V |
50 | 48, 49 | brcnv 5839 |
. . . . 5
β’ (πβ‘ < π β π < π) |
51 | 50 | notbii 320 |
. . . 4
β’ (Β¬
πβ‘ < π β Β¬ π < π) |
52 | 51 | ralbii 3093 |
. . 3
β’
(βπ β
π΄ Β¬ πβ‘
<
π β βπ β π΄ Β¬ π < π) |
53 | 49, 48 | brcnv 5839 |
. . . . 5
β’ (πβ‘ < π β π < π) |
54 | | vex 3448 |
. . . . . . 7
β’ π β V |
55 | 49, 54 | brcnv 5839 |
. . . . . 6
β’ (πβ‘ < π β π < π) |
56 | 55 | rexbii 3094 |
. . . . 5
β’
(βπ β
π΄ πβ‘
<
π β βπ β π΄ π < π) |
57 | 53, 56 | imbi12i 351 |
. . . 4
β’ ((πβ‘ < π β βπ β π΄ πβ‘
<
π) β (π < π β βπ β π΄ π < π)) |
58 | 57 | ralbii 3093 |
. . 3
β’
(βπ β
π΅ (πβ‘
<
π β βπ β π΄ πβ‘
<
π) β βπ β π΅ (π < π β βπ β π΄ π < π)) |
59 | 52, 58 | anbi12i 628 |
. 2
β’
((βπ β
π΄ Β¬ πβ‘
<
π β§ βπ β π΅ (πβ‘
<
π β βπ β π΄ πβ‘
<
π)) β (βπ β π΄ Β¬ π < π β§ βπ β π΅ (π < π β βπ β π΄ π < π))) |
60 | 47, 59 | bitr4di 289 |
1
β’ ((π β§ π β π΅) β ((βπ β π΄ π β€ π β§ βπ β π΅ (βπ β π΄ π β€ π β π β€ π)) β (βπ β π΄ Β¬ πβ‘
<
π β§ βπ β π΅ (πβ‘
<
π β βπ β π΄ πβ‘
<
π)))) |