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 ∧ 𝑆 ⊆ 𝐴 ) → 𝑆 ⊆ ( 𝑀 ‘ ( 𝑈 ‘ 𝑆 ) ) )