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 𝑈 = ( lub ‘ 𝐾 )
sspmaplub.a 𝐴 = ( Atoms ‘ 𝐾 )
sspmaplub.m 𝑀 = ( pmap ‘ 𝐾 )
Assertion sspmaplubN ( ( 𝐾 ∈ HL ∧ 𝑆𝐴 ) → 𝑆 ⊆ ( 𝑀 ‘ ( 𝑈𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 sspmaplub.u 𝑈 = ( lub ‘ 𝐾 )
2 sspmaplub.a 𝐴 = ( Atoms ‘ 𝐾 )
3 sspmaplub.m 𝑀 = ( pmap ‘ 𝐾 )
4 eqid ( ⊥𝑃𝐾 ) = ( ⊥𝑃𝐾 )
5 2 4 2polssN ( ( 𝐾 ∈ HL ∧ 𝑆𝐴 ) → 𝑆 ⊆ ( ( ⊥𝑃𝐾 ) ‘ ( ( ⊥𝑃𝐾 ) ‘ 𝑆 ) ) )
6 1 2 3 4 2polvalN ( ( 𝐾 ∈ HL ∧ 𝑆𝐴 ) → ( ( ⊥𝑃𝐾 ) ‘ ( ( ⊥𝑃𝐾 ) ‘ 𝑆 ) ) = ( 𝑀 ‘ ( 𝑈𝑆 ) ) )
7 5 6 sseqtrd ( ( 𝐾 ∈ HL ∧ 𝑆𝐴 ) → 𝑆 ⊆ ( 𝑀 ‘ ( 𝑈𝑆 ) ) )