Step |
Hyp |
Ref |
Expression |
1 |
|
pmaplub.b |
|- B = ( Base ` K ) |
2 |
|
pmaplub.u |
|- U = ( lub ` K ) |
3 |
|
pmaplub.m |
|- M = ( pmap ` K ) |
4 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
5 |
|
eqid |
|- ( Atoms ` K ) = ( Atoms ` K ) |
6 |
1 4 5 3
|
pmapval |
|- ( ( K e. HL /\ X e. B ) -> ( M ` X ) = { p e. ( Atoms ` K ) | p ( le ` K ) X } ) |
7 |
6
|
fveq2d |
|- ( ( K e. HL /\ X e. B ) -> ( U ` ( M ` X ) ) = ( U ` { p e. ( Atoms ` K ) | p ( le ` K ) X } ) ) |
8 |
|
hlomcmat |
|- ( K e. HL -> ( K e. OML /\ K e. CLat /\ K e. AtLat ) ) |
9 |
1 4 2 5
|
atlatmstc |
|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( U ` { p e. ( Atoms ` K ) | p ( le ` K ) X } ) = X ) |
10 |
8 9
|
sylan |
|- ( ( K e. HL /\ X e. B ) -> ( U ` { p e. ( Atoms ` K ) | p ( le ` K ) X } ) = X ) |
11 |
7 10
|
eqtrd |
|- ( ( K e. HL /\ X e. B ) -> ( U ` ( M ` X ) ) = X ) |