Metamath Proof Explorer


Theorem sspmaplubN

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 ) ) )

Proof

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 ) ) )