Step | Hyp | Ref
| Expression |
1 | | opposet 37689 |
. . . 4
β’ (πΎ β OP β πΎ β Poset) |
2 | 1 | 3ad2ant1 1134 |
. . 3
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β πΎ β Poset) |
3 | | simp1 1137 |
. . . 4
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β πΎ β OP) |
4 | | simp22 1208 |
. . . 4
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β π β π΅) |
5 | | cvrcmp.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
6 | | eqid 2733 |
. . . . 5
β’
(ocβπΎ) =
(ocβπΎ) |
7 | 5, 6 | opoccl 37702 |
. . . 4
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
8 | 3, 4, 7 | syl2anc 585 |
. . 3
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β ((ocβπΎ)βπ) β π΅) |
9 | | simp21 1207 |
. . . 4
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β π β π΅) |
10 | 5, 6 | opoccl 37702 |
. . . 4
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
11 | 3, 9, 10 | syl2anc 585 |
. . 3
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β ((ocβπΎ)βπ) β π΅) |
12 | | simp23 1209 |
. . . 4
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β π β π΅) |
13 | 5, 6 | opoccl 37702 |
. . . 4
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
14 | 3, 12, 13 | syl2anc 585 |
. . 3
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β ((ocβπΎ)βπ) β π΅) |
15 | | cvrcmp.c |
. . . . . . . 8
β’ πΆ = ( β βπΎ) |
16 | 5, 6, 15 | cvrcon3b 37785 |
. . . . . . 7
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (ππΆπ β ((ocβπΎ)βπ)πΆ((ocβπΎ)βπ))) |
17 | 16 | 3adant3r2 1184 |
. . . . . 6
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (ππΆπ β ((ocβπΎ)βπ)πΆ((ocβπΎ)βπ))) |
18 | 5, 6, 15 | cvrcon3b 37785 |
. . . . . . 7
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (ππΆπ β ((ocβπΎ)βπ)πΆ((ocβπΎ)βπ))) |
19 | 18 | 3adant3r1 1183 |
. . . . . 6
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (ππΆπ β ((ocβπΎ)βπ)πΆ((ocβπΎ)βπ))) |
20 | 17, 19 | anbi12d 632 |
. . . . 5
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ππΆπ β§ ππΆπ) β (((ocβπΎ)βπ)πΆ((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)πΆ((ocβπΎ)βπ)))) |
21 | 20 | biimp3a 1470 |
. . . 4
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (((ocβπΎ)βπ)πΆ((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)πΆ((ocβπΎ)βπ))) |
22 | 21 | ancomd 463 |
. . 3
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (((ocβπΎ)βπ)πΆ((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)πΆ((ocβπΎ)βπ))) |
23 | | cvrcmp.l |
. . . 4
β’ β€ =
(leβπΎ) |
24 | 5, 23, 15 | cvrcmp 37791 |
. . 3
β’ ((πΎ β Poset β§
(((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅) β§ (((ocβπΎ)βπ)πΆ((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)πΆ((ocβπΎ)βπ))) β (((ocβπΎ)βπ) β€ ((ocβπΎ)βπ) β ((ocβπΎ)βπ) = ((ocβπΎ)βπ))) |
25 | 2, 8, 11, 14, 22, 24 | syl131anc 1384 |
. 2
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (((ocβπΎ)βπ) β€ ((ocβπΎ)βπ) β ((ocβπΎ)βπ) = ((ocβπΎ)βπ))) |
26 | 5, 23, 6 | oplecon3b 37708 |
. . 3
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π β€ π β ((ocβπΎ)βπ) β€ ((ocβπΎ)βπ))) |
27 | 3, 9, 4, 26 | syl3anc 1372 |
. 2
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β€ π β ((ocβπΎ)βπ) β€ ((ocβπΎ)βπ))) |
28 | 5, 6 | opcon3b 37704 |
. . 3
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π = π β ((ocβπΎ)βπ) = ((ocβπΎ)βπ))) |
29 | 3, 9, 4, 28 | syl3anc 1372 |
. 2
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π = π β ((ocβπΎ)βπ) = ((ocβπΎ)βπ))) |
30 | 25, 27, 29 | 3bitr4d 311 |
1
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β€ π β π = π)) |