Description: A set of atoms is a subset of the projective map of its LUB. (Contributed by NM, 6-Mar-2012) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sspmaplub.u | |- U = ( lub ` K ) |
|
sspmaplub.a | |- A = ( Atoms ` K ) |
||
sspmaplub.m | |- M = ( pmap ` K ) |
||
Assertion | sspmaplubN | |- ( ( K e. HL /\ S C_ A ) -> S C_ ( M ` ( U ` S ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sspmaplub.u | |- U = ( lub ` K ) |
|
2 | sspmaplub.a | |- A = ( Atoms ` K ) |
|
3 | sspmaplub.m | |- M = ( pmap ` K ) |
|
4 | eqid | |- ( _|_P ` K ) = ( _|_P ` K ) |
|
5 | 2 4 | 2polssN | |- ( ( K e. HL /\ S C_ A ) -> S C_ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` S ) ) ) |
6 | 1 2 3 4 | 2polvalN | |- ( ( K e. HL /\ S C_ A ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` S ) ) = ( M ` ( U ` S ) ) ) |
7 | 5 6 | sseqtrd | |- ( ( K e. HL /\ S C_ A ) -> S C_ ( M ` ( U ` S ) ) ) |