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