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 HL S A S 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 𝑃 K = 𝑃 K
5 2 4 2polssN K HL S A S 𝑃 K 𝑃 K S
6 1 2 3 4 2polvalN K HL S A 𝑃 K 𝑃 K S = M U S
7 5 6 sseqtrd K HL S A S M U S