Step | Hyp | Ref
| Expression |
1 | | cvrletr.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
2 | | cvrletr.s |
. . . . . 6
β’ < =
(ltβπΎ) |
3 | | cvrletr.c |
. . . . . 6
β’ πΆ = ( β βπΎ) |
4 | 1, 2, 3 | cvrnbtwn 37779 |
. . . . 5
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β Β¬ (π < π β§ π < π)) |
5 | 4 | 3expia 1122 |
. . . 4
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (ππΆπ β Β¬ (π < π β§ π < π))) |
6 | | iman 403 |
. . . . 5
β’ (((π < π β§ π β€ π) β π = π) β Β¬ ((π < π β§ π β€ π) β§ Β¬ π = π)) |
7 | | anass 470 |
. . . . . . 7
β’ (((π < π β§ π β€ π) β§ Β¬ π = π) β (π < π β§ (π β€ π β§ Β¬ π = π))) |
8 | | simpl 484 |
. . . . . . . . . 10
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β Poset) |
9 | | simpr3 1197 |
. . . . . . . . . 10
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
10 | | simpr2 1196 |
. . . . . . . . . 10
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
11 | | cvrletr.l |
. . . . . . . . . . 11
β’ β€ =
(leβπΎ) |
12 | 11, 2 | pltval 18226 |
. . . . . . . . . 10
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π < π β (π β€ π β§ π β π))) |
13 | 8, 9, 10, 12 | syl3anc 1372 |
. . . . . . . . 9
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π < π β (π β€ π β§ π β π))) |
14 | | df-ne 2941 |
. . . . . . . . . 10
β’ (π β π β Β¬ π = π) |
15 | 14 | anbi2i 624 |
. . . . . . . . 9
β’ ((π β€ π β§ π β π) β (π β€ π β§ Β¬ π = π)) |
16 | 13, 15 | bitrdi 287 |
. . . . . . . 8
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π < π β (π β€ π β§ Β¬ π = π))) |
17 | 16 | anbi2d 630 |
. . . . . . 7
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π < π β§ π < π) β (π < π β§ (π β€ π β§ Β¬ π = π)))) |
18 | 7, 17 | bitr4id 290 |
. . . . . 6
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((π < π β§ π β€ π) β§ Β¬ π = π) β (π < π β§ π < π))) |
19 | 18 | notbid 318 |
. . . . 5
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (Β¬ ((π < π β§ π β€ π) β§ Β¬ π = π) β Β¬ (π < π β§ π < π))) |
20 | 6, 19 | bitr2id 284 |
. . . 4
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (Β¬ (π < π β§ π < π) β ((π < π β§ π β€ π) β π = π))) |
21 | 5, 20 | sylibd 238 |
. . 3
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (ππΆπ β ((π < π β§ π β€ π) β π = π))) |
22 | 21 | 3impia 1118 |
. 2
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β ((π < π β§ π β€ π) β π = π)) |
23 | 1, 2, 3 | cvrlt 37778 |
. . . . . . 7
β’ (((πΎ β Poset β§ π β π΅ β§ π β π΅) β§ ππΆπ) β π < π) |
24 | 23 | ex 414 |
. . . . . 6
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (ππΆπ β π < π)) |
25 | 24 | 3adant3r3 1185 |
. . . . 5
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (ππΆπ β π < π)) |
26 | 25 | 3impia 1118 |
. . . 4
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β π < π) |
27 | | breq2 5110 |
. . . 4
β’ (π = π β (π < π β π < π)) |
28 | 26, 27 | syl5ibrcom 247 |
. . 3
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β (π = π β π < π)) |
29 | 1, 11 | posref 18212 |
. . . . . 6
β’ ((πΎ β Poset β§ π β π΅) β π β€ π) |
30 | 29 | 3ad2antr2 1190 |
. . . . 5
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β€ π) |
31 | | breq1 5109 |
. . . . 5
β’ (π = π β (π β€ π β π β€ π)) |
32 | 30, 31 | syl5ibrcom 247 |
. . . 4
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π = π β π β€ π)) |
33 | 32 | 3adant3 1133 |
. . 3
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β (π = π β π β€ π)) |
34 | 28, 33 | jcad 514 |
. 2
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β (π = π β (π < π β§ π β€ π))) |
35 | 22, 34 | impbid 211 |
1
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β ((π < π β§ π β€ π) β π = π)) |