Step | Hyp | Ref
| Expression |
1 | | opcon3.b |
. . 3
β’ π΅ = (BaseβπΎ) |
2 | | opcon3.l |
. . 3
β’ β€ =
(leβπΎ) |
3 | | opcon3.o |
. . 3
β’ β₯ =
(ocβπΎ) |
4 | 1, 2, 3 | oplecon3 37664 |
. 2
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π β€ π β ( β₯ βπ) β€ ( β₯ βπ))) |
5 | | simp1 1137 |
. . . 4
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β πΎ β OP) |
6 | 1, 3 | opoccl 37659 |
. . . . 5
β’ ((πΎ β OP β§ π β π΅) β ( β₯ βπ) β π΅) |
7 | 6 | 3adant2 1132 |
. . . 4
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β ( β₯ βπ) β π΅) |
8 | 1, 3 | opoccl 37659 |
. . . . 5
β’ ((πΎ β OP β§ π β π΅) β ( β₯ βπ) β π΅) |
9 | 8 | 3adant3 1133 |
. . . 4
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β ( β₯ βπ) β π΅) |
10 | 1, 2, 3 | oplecon3 37664 |
. . . 4
β’ ((πΎ β OP β§ ( β₯
βπ) β π΅ β§ ( β₯ βπ) β π΅) β (( β₯ βπ) β€ ( β₯ βπ) β ( β₯ β( β₯
βπ)) β€ ( β₯
β( β₯ βπ)))) |
11 | 5, 7, 9, 10 | syl3anc 1372 |
. . 3
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (( β₯ βπ) β€ ( β₯ βπ) β ( β₯ β( β₯
βπ)) β€ ( β₯
β( β₯ βπ)))) |
12 | 1, 3 | opococ 37660 |
. . . . 5
β’ ((πΎ β OP β§ π β π΅) β ( β₯ β( β₯
βπ)) = π) |
13 | 12 | 3adant3 1133 |
. . . 4
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β ( β₯ β( β₯
βπ)) = π) |
14 | 1, 3 | opococ 37660 |
. . . . 5
β’ ((πΎ β OP β§ π β π΅) β ( β₯ β( β₯
βπ)) = π) |
15 | 14 | 3adant2 1132 |
. . . 4
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β ( β₯ β( β₯
βπ)) = π) |
16 | 13, 15 | breq12d 5119 |
. . 3
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (( β₯ β( β₯
βπ)) β€ ( β₯
β( β₯ βπ)) β π β€ π)) |
17 | 11, 16 | sylibd 238 |
. 2
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (( β₯ βπ) β€ ( β₯ βπ) β π β€ π)) |
18 | 4, 17 | impbid 211 |
1
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π β€ π β ( β₯ βπ) β€ ( β₯ βπ))) |