Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . . . . 6
β’
(leβπΎ) =
(leβπΎ) |
2 | | pltnlt.s |
. . . . . 6
β’ < =
(ltβπΎ) |
3 | 1, 2 | pltle 18290 |
. . . . 5
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π < π β π(leβπΎ)π)) |
4 | 3 | 3adant3r3 1184 |
. . . 4
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π < π β π(leβπΎ)π)) |
5 | 1, 2 | pltle 18290 |
. . . . 5
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π < π β π(leβπΎ)π)) |
6 | 5 | 3adant3r1 1182 |
. . . 4
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π < π β π(leβπΎ)π)) |
7 | | pltnlt.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
8 | 7, 1 | postr 18277 |
. . . 4
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)) |
9 | 4, 6, 8 | syl2and 608 |
. . 3
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π < π β§ π < π) β π(leβπΎ)π)) |
10 | 7, 2 | pltn2lp 18298 |
. . . . . 6
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β Β¬ (π < π β§ π < π)) |
11 | 10 | 3adant3r3 1184 |
. . . . 5
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β Β¬ (π < π β§ π < π)) |
12 | | breq2 5152 |
. . . . . . 7
β’ (π = π β (π < π β π < π)) |
13 | 12 | anbi2d 629 |
. . . . . 6
β’ (π = π β ((π < π β§ π < π) β (π < π β§ π < π))) |
14 | 13 | notbid 317 |
. . . . 5
β’ (π = π β (Β¬ (π < π β§ π < π) β Β¬ (π < π β§ π < π))) |
15 | 11, 14 | syl5ibcom 244 |
. . . 4
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π = π β Β¬ (π < π β§ π < π))) |
16 | 15 | necon2ad 2955 |
. . 3
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π < π β§ π < π) β π β π)) |
17 | 9, 16 | jcad 513 |
. 2
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π < π β§ π < π) β (π(leβπΎ)π β§ π β π))) |
18 | 1, 2 | pltval 18289 |
. . 3
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π < π β (π(leβπΎ)π β§ π β π))) |
19 | 18 | 3adant3r2 1183 |
. 2
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π < π β (π(leβπΎ)π β§ π β π))) |
20 | 17, 19 | sylibrd 258 |
1
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π < π β§ π < π) β π < π)) |