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