Step | Hyp | Ref
| Expression |
1 | | cvrle.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | eqid 2733 |
. . . 4
β’
(ltβπΎ) =
(ltβπΎ) |
3 | | cvrle.c |
. . . 4
β’ πΆ = ( β βπΎ) |
4 | 1, 2, 3 | cvrnbtwn 37779 |
. . 3
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β Β¬ (π(ltβπΎ)π β§ π(ltβπΎ)π)) |
5 | | iman 403 |
. . . . 5
β’ (((π β€ π β§ π β€ π) β (π = π β¨ π = π)) β Β¬ ((π β€ π β§ π β€ π) β§ Β¬ (π = π β¨ π = π))) |
6 | | neanior 3034 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β Β¬ (π = π β¨ π = π)) |
7 | 6 | anbi2i 624 |
. . . . . . . 8
β’ (((π β€ π β§ π β€ π) β§ (π β π β§ π β π)) β ((π β€ π β§ π β€ π) β§ Β¬ (π = π β¨ π = π))) |
8 | | an4 655 |
. . . . . . . 8
β’ (((π β€ π β§ π β€ π) β§ (π β π β§ π β π)) β ((π β€ π β§ π β π) β§ (π β€ π β§ π β π))) |
9 | 7, 8 | bitr3i 277 |
. . . . . . 7
β’ (((π β€ π β§ π β€ π) β§ Β¬ (π = π β¨ π = π)) β ((π β€ π β§ π β π) β§ (π β€ π β§ π β π))) |
10 | | cvrle.l |
. . . . . . . . . 10
β’ β€ =
(leβπΎ) |
11 | 10, 2 | pltval 18226 |
. . . . . . . . 9
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π(ltβπΎ)π β (π β€ π β§ π β π))) |
12 | 11 | 3adant3r2 1184 |
. . . . . . . 8
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π(ltβπΎ)π β (π β€ π β§ π β π))) |
13 | 10, 2 | pltval 18226 |
. . . . . . . . . 10
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π(ltβπΎ)π β (π β€ π β§ π β π))) |
14 | 13 | 3com23 1127 |
. . . . . . . . 9
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π(ltβπΎ)π β (π β€ π β§ π β π))) |
15 | 14 | 3adant3r1 1183 |
. . . . . . . 8
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π(ltβπΎ)π β (π β€ π β§ π β π))) |
16 | 12, 15 | anbi12d 632 |
. . . . . . 7
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π(ltβπΎ)π β§ π(ltβπΎ)π) β ((π β€ π β§ π β π) β§ (π β€ π β§ π β π)))) |
17 | 9, 16 | bitr4id 290 |
. . . . . 6
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((π β€ π β§ π β€ π) β§ Β¬ (π = π β¨ π = π)) β (π(ltβπΎ)π β§ π(ltβπΎ)π))) |
18 | 17 | notbid 318 |
. . . . 5
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (Β¬ ((π β€ π β§ π β€ π) β§ Β¬ (π = π β¨ π = π)) β Β¬ (π(ltβπΎ)π β§ π(ltβπΎ)π))) |
19 | 5, 18 | bitr2id 284 |
. . . 4
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (Β¬ (π(ltβπΎ)π β§ π(ltβπΎ)π) β ((π β€ π β§ π β€ π) β (π = π β¨ π = π)))) |
20 | 19 | 3adant3 1133 |
. . 3
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β (Β¬ (π(ltβπΎ)π β§ π(ltβπΎ)π) β ((π β€ π β§ π β€ π) β (π = π β¨ π = π)))) |
21 | 4, 20 | mpbid 231 |
. 2
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β ((π β€ π β§ π β€ π) β (π = π β¨ π = π))) |
22 | 1, 10 | posref 18212 |
. . . . . . 7
β’ ((πΎ β Poset β§ π β π΅) β π β€ π) |
23 | 22 | 3ad2antr3 1191 |
. . . . . 6
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β€ π) |
24 | 23 | 3adant3 1133 |
. . . . 5
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β π β€ π) |
25 | | breq1 5109 |
. . . . 5
β’ (π = π β (π β€ π β π β€ π)) |
26 | 24, 25 | syl5ibrcom 247 |
. . . 4
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β (π = π β π β€ π)) |
27 | 1, 10, 3 | cvrle 37786 |
. . . . . . . 8
β’ (((πΎ β Poset β§ π β π΅ β§ π β π΅) β§ ππΆπ) β π β€ π) |
28 | 27 | ex 414 |
. . . . . . 7
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (ππΆπ β π β€ π)) |
29 | 28 | 3adant3r3 1185 |
. . . . . 6
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (ππΆπ β π β€ π)) |
30 | 29 | 3impia 1118 |
. . . . 5
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β π β€ π) |
31 | | breq2 5110 |
. . . . 5
β’ (π = π β (π β€ π β π β€ π)) |
32 | 30, 31 | syl5ibrcom 247 |
. . . 4
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β (π = π β π β€ π)) |
33 | 26, 32 | jaod 858 |
. . 3
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β ((π = π β¨ π = π) β π β€ π)) |
34 | | breq1 5109 |
. . . . 5
β’ (π = π β (π β€ π β π β€ π)) |
35 | 30, 34 | syl5ibcom 244 |
. . . 4
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β (π = π β π β€ π)) |
36 | | breq2 5110 |
. . . . 5
β’ (π = π β (π β€ π β π β€ π)) |
37 | 24, 36 | syl5ibcom 244 |
. . . 4
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β (π = π β π β€ π)) |
38 | 35, 37 | jaod 858 |
. . 3
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β ((π = π β¨ π = π) β π β€ π)) |
39 | 33, 38 | jcad 514 |
. 2
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β ((π = π β¨ π = π) β (π β€ π β§ π β€ π))) |
40 | 21, 39 | impbid 211 |
1
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ ππΆπ) β ((π β€ π β§ π β€ π) β (π = π β¨ π = π))) |