Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . . 4
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
2 | | isoml.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
3 | 1, 2 | eqtr4di 2795 |
. . 3
β’ (π = πΎ β (Baseβπ) = π΅) |
4 | | fveq2 6843 |
. . . . . . 7
β’ (π = πΎ β (leβπ) = (leβπΎ)) |
5 | | isoml.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
6 | 4, 5 | eqtr4di 2795 |
. . . . . 6
β’ (π = πΎ β (leβπ) = β€ ) |
7 | 6 | breqd 5117 |
. . . . 5
β’ (π = πΎ β (π₯(leβπ)π¦ β π₯ β€ π¦)) |
8 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΎ β (joinβπ) = (joinβπΎ)) |
9 | | isoml.j |
. . . . . . . 8
β’ β¨ =
(joinβπΎ) |
10 | 8, 9 | eqtr4di 2795 |
. . . . . . 7
β’ (π = πΎ β (joinβπ) = β¨ ) |
11 | | eqidd 2738 |
. . . . . . 7
β’ (π = πΎ β π₯ = π₯) |
12 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = πΎ β (meetβπ) = (meetβπΎ)) |
13 | | isoml.m |
. . . . . . . . 9
β’ β§ =
(meetβπΎ) |
14 | 12, 13 | eqtr4di 2795 |
. . . . . . . 8
β’ (π = πΎ β (meetβπ) = β§ ) |
15 | | eqidd 2738 |
. . . . . . . 8
β’ (π = πΎ β π¦ = π¦) |
16 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = πΎ β (ocβπ) = (ocβπΎ)) |
17 | | isoml.o |
. . . . . . . . . 10
β’ β₯ =
(ocβπΎ) |
18 | 16, 17 | eqtr4di 2795 |
. . . . . . . . 9
β’ (π = πΎ β (ocβπ) = β₯ ) |
19 | 18 | fveq1d 6845 |
. . . . . . . 8
β’ (π = πΎ β ((ocβπ)βπ₯) = ( β₯ βπ₯)) |
20 | 14, 15, 19 | oveq123d 7379 |
. . . . . . 7
β’ (π = πΎ β (π¦(meetβπ)((ocβπ)βπ₯)) = (π¦ β§ ( β₯ βπ₯))) |
21 | 10, 11, 20 | oveq123d 7379 |
. . . . . 6
β’ (π = πΎ β (π₯(joinβπ)(π¦(meetβπ)((ocβπ)βπ₯))) = (π₯ β¨ (π¦ β§ ( β₯ βπ₯)))) |
22 | 21 | eqeq2d 2748 |
. . . . 5
β’ (π = πΎ β (π¦ = (π₯(joinβπ)(π¦(meetβπ)((ocβπ)βπ₯))) β π¦ = (π₯ β¨ (π¦ β§ ( β₯ βπ₯))))) |
23 | 7, 22 | imbi12d 345 |
. . . 4
β’ (π = πΎ β ((π₯(leβπ)π¦ β π¦ = (π₯(joinβπ)(π¦(meetβπ)((ocβπ)βπ₯)))) β (π₯ β€ π¦ β π¦ = (π₯ β¨ (π¦ β§ ( β₯ βπ₯)))))) |
24 | 3, 23 | raleqbidv 3320 |
. . 3
β’ (π = πΎ β (βπ¦ β (Baseβπ)(π₯(leβπ)π¦ β π¦ = (π₯(joinβπ)(π¦(meetβπ)((ocβπ)βπ₯)))) β βπ¦ β π΅ (π₯ β€ π¦ β π¦ = (π₯ β¨ (π¦ β§ ( β₯ βπ₯)))))) |
25 | 3, 24 | raleqbidv 3320 |
. 2
β’ (π = πΎ β (βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(π₯(leβπ)π¦ β π¦ = (π₯(joinβπ)(π¦(meetβπ)((ocβπ)βπ₯)))) β βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β π¦ = (π₯ β¨ (π¦ β§ ( β₯ βπ₯)))))) |
26 | | df-oml 37644 |
. 2
β’ OML =
{π β OL β£
βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)(π₯(leβπ)π¦ β π¦ = (π₯(joinβπ)(π¦(meetβπ)((ocβπ)βπ₯))))} |
27 | 25, 26 | elrab2 3649 |
1
β’ (πΎ β OML β (πΎ β OL β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β π¦ = (π₯ β¨ (π¦ β§ ( β₯ βπ₯)))))) |