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=\mathrm{lub}\left(K\right)$$
	sspmaplub.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	sspmaplub.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
Assertion	sspmaplubN	$$⊢\left(K\in \mathrm{HL}\wedge S\subseteq A\right)\to S\subseteq M\left(U\left(S\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sspmaplub.u	$$⊢U=\mathrm{lub}\left(K\right)$$
2		sspmaplub.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3		sspmaplub.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
4		eqid	$$⊢{\perp }_{𝑃}\left(K\right)={\perp }_{𝑃}\left(K\right)$$
5	2 4	2polssN	$$⊢\left(K\in \mathrm{HL}\wedge S\subseteq A\right)\to S\subseteq {\perp }_{𝑃}\left(K\right)\left({\perp }_{𝑃}\left(K\right)\left(S\right)\right)$$
6	1 2 3 4	2polvalN	$$⊢\left(K\in \mathrm{HL}\wedge S\subseteq A\right)\to {\perp }_{𝑃}\left(K\right)\left({\perp }_{𝑃}\left(K\right)\left(S\right)\right)=M\left(U\left(S\right)\right)$$
7	5 6	sseqtrd	$$⊢\left(K\in \mathrm{HL}\wedge S\subseteq A\right)\to S\subseteq M\left(U\left(S\right)\right)$$