Step | Hyp | Ref
| Expression |
1 | | oposlem.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
2 | | eqid 2737 |
. . . . 5
β’
(lubβπΎ) =
(lubβπΎ) |
3 | | eqid 2737 |
. . . . 5
β’
(glbβπΎ) =
(glbβπΎ) |
4 | | oposlem.l |
. . . . 5
β’ β€ =
(leβπΎ) |
5 | | oposlem.o |
. . . . 5
β’ β₯ =
(ocβπΎ) |
6 | | oposlem.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
7 | | oposlem.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
8 | | oposlem.f |
. . . . 5
β’ 0 =
(0.βπΎ) |
9 | | oposlem.u |
. . . . 5
β’ 1 =
(1.βπΎ) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | isopos 37645 |
. . . 4
β’ (πΎ β OP β ((πΎ β Poset β§ π΅ β dom (lubβπΎ) β§ π΅ β dom (glbβπΎ)) β§ βπ₯ β π΅ βπ¦ β π΅ ((( β₯ βπ₯) β π΅ β§ ( β₯ β( β₯
βπ₯)) = π₯ β§ (π₯ β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ₯))) β§ (π₯ β¨ ( β₯ βπ₯)) = 1 β§ (π₯ β§ ( β₯ βπ₯)) = 0 ))) |
11 | 10 | simprbi 498 |
. . 3
β’ (πΎ β OP β βπ₯ β π΅ βπ¦ β π΅ ((( β₯ βπ₯) β π΅ β§ ( β₯ β( β₯
βπ₯)) = π₯ β§ (π₯ β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ₯))) β§ (π₯ β¨ ( β₯ βπ₯)) = 1 β§ (π₯ β§ ( β₯ βπ₯)) = 0 )) |
12 | | fveq2 6843 |
. . . . . . 7
β’ (π₯ = π β ( β₯ βπ₯) = ( β₯ βπ)) |
13 | 12 | eleq1d 2823 |
. . . . . 6
β’ (π₯ = π β (( β₯ βπ₯) β π΅ β ( β₯ βπ) β π΅)) |
14 | | 2fveq3 6848 |
. . . . . . 7
β’ (π₯ = π β ( β₯ β( β₯
βπ₯)) = ( β₯
β( β₯ βπ))) |
15 | | id 22 |
. . . . . . 7
β’ (π₯ = π β π₯ = π) |
16 | 14, 15 | eqeq12d 2753 |
. . . . . 6
β’ (π₯ = π β (( β₯ β( β₯
βπ₯)) = π₯ β ( β₯ β( β₯
βπ)) = π)) |
17 | | breq1 5109 |
. . . . . . 7
β’ (π₯ = π β (π₯ β€ π¦ β π β€ π¦)) |
18 | 12 | breq2d 5118 |
. . . . . . 7
β’ (π₯ = π β (( β₯ βπ¦) β€ ( β₯ βπ₯) β ( β₯ βπ¦) β€ ( β₯ βπ))) |
19 | 17, 18 | imbi12d 345 |
. . . . . 6
β’ (π₯ = π β ((π₯ β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ₯)) β (π β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ)))) |
20 | 13, 16, 19 | 3anbi123d 1437 |
. . . . 5
β’ (π₯ = π β ((( β₯ βπ₯) β π΅ β§ ( β₯ β( β₯
βπ₯)) = π₯ β§ (π₯ β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ₯))) β (( β₯ βπ) β π΅ β§ ( β₯ β( β₯
βπ)) = π β§ (π β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ))))) |
21 | 15, 12 | oveq12d 7376 |
. . . . . 6
β’ (π₯ = π β (π₯ β¨ ( β₯ βπ₯)) = (π β¨ ( β₯ βπ))) |
22 | 21 | eqeq1d 2739 |
. . . . 5
β’ (π₯ = π β ((π₯ β¨ ( β₯ βπ₯)) = 1 β (π β¨ ( β₯ βπ)) = 1 )) |
23 | 15, 12 | oveq12d 7376 |
. . . . . 6
β’ (π₯ = π β (π₯ β§ ( β₯ βπ₯)) = (π β§ ( β₯ βπ))) |
24 | 23 | eqeq1d 2739 |
. . . . 5
β’ (π₯ = π β ((π₯ β§ ( β₯ βπ₯)) = 0 β (π β§ ( β₯ βπ)) = 0 )) |
25 | 20, 22, 24 | 3anbi123d 1437 |
. . . 4
β’ (π₯ = π β (((( β₯ βπ₯) β π΅ β§ ( β₯ β( β₯
βπ₯)) = π₯ β§ (π₯ β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ₯))) β§ (π₯ β¨ ( β₯ βπ₯)) = 1 β§ (π₯ β§ ( β₯ βπ₯)) = 0 ) β ((( β₯
βπ) β π΅ β§ ( β₯ β( β₯
βπ)) = π β§ (π β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ))) β§ (π β¨ ( β₯ βπ)) = 1 β§ (π β§ ( β₯ βπ)) = 0 ))) |
26 | | breq2 5110 |
. . . . . . 7
β’ (π¦ = π β (π β€ π¦ β π β€ π)) |
27 | | fveq2 6843 |
. . . . . . . 8
β’ (π¦ = π β ( β₯ βπ¦) = ( β₯ βπ)) |
28 | 27 | breq1d 5116 |
. . . . . . 7
β’ (π¦ = π β (( β₯ βπ¦) β€ ( β₯ βπ) β ( β₯ βπ) β€ ( β₯ βπ))) |
29 | 26, 28 | imbi12d 345 |
. . . . . 6
β’ (π¦ = π β ((π β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ)) β (π β€ π β ( β₯ βπ) β€ ( β₯ βπ)))) |
30 | 29 | 3anbi3d 1443 |
. . . . 5
β’ (π¦ = π β ((( β₯ βπ) β π΅ β§ ( β₯ β( β₯
βπ)) = π β§ (π β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ))) β (( β₯ βπ) β π΅ β§ ( β₯ β( β₯
βπ)) = π β§ (π β€ π β ( β₯ βπ) β€ ( β₯ βπ))))) |
31 | 30 | 3anbi1d 1441 |
. . . 4
β’ (π¦ = π β (((( β₯ βπ) β π΅ β§ ( β₯ β( β₯
βπ)) = π β§ (π β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ))) β§ (π β¨ ( β₯ βπ)) = 1 β§ (π β§ ( β₯ βπ)) = 0 ) β ((( β₯
βπ) β π΅ β§ ( β₯ β( β₯
βπ)) = π β§ (π β€ π β ( β₯ βπ) β€ ( β₯ βπ))) β§ (π β¨ ( β₯ βπ)) = 1 β§ (π β§ ( β₯ βπ)) = 0 ))) |
32 | 25, 31 | rspc2v 3591 |
. . 3
β’ ((π β π΅ β§ π β π΅) β (βπ₯ β π΅ βπ¦ β π΅ ((( β₯ βπ₯) β π΅ β§ ( β₯ β( β₯
βπ₯)) = π₯ β§ (π₯ β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ₯))) β§ (π₯ β¨ ( β₯ βπ₯)) = 1 β§ (π₯ β§ ( β₯ βπ₯)) = 0 ) β ((( β₯
βπ) β π΅ β§ ( β₯ β( β₯
βπ)) = π β§ (π β€ π β ( β₯ βπ) β€ ( β₯ βπ))) β§ (π β¨ ( β₯ βπ)) = 1 β§ (π β§ ( β₯ βπ)) = 0 ))) |
33 | 11, 32 | mpan9 508 |
. 2
β’ ((πΎ β OP β§ (π β π΅ β§ π β π΅)) β ((( β₯ βπ) β π΅ β§ ( β₯ β( β₯
βπ)) = π β§ (π β€ π β ( β₯ βπ) β€ ( β₯ βπ))) β§ (π β¨ ( β₯ βπ)) = 1 β§ (π β§ ( β₯ βπ)) = 0 )) |
34 | 33 | 3impb 1116 |
1
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β ((( β₯ βπ) β π΅ β§ ( β₯ β( β₯
βπ)) = π β§ (π β€ π β ( β₯ βπ) β€ ( β₯ βπ))) β§ (π β¨ ( β₯ βπ)) = 1 β§ (π β§ ( β₯ βπ)) = 0 )) |