Metamath Proof Explorer


Theorem 2polssN

Description: A set of atoms is a subset of its double polarity. (Contributed by NM, 29-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2polss.a A = Atoms K
2polss.p ˙ = 𝑃 K
Assertion 2polssN K HL X A X ˙ ˙ X

Proof

Step Hyp Ref Expression
1 2polss.a A = Atoms K
2 2polss.p ˙ = 𝑃 K
3 hlclat K HL K CLat
4 3 ad3antrrr K HL X A p A p X K CLat
5 simpr K HL X A p A p X p X
6 simpllr K HL X A p A p X X A
7 eqid Base K = Base K
8 7 1 atssbase A Base K
9 6 8 sstrdi K HL X A p A p X X Base K
10 eqid K = K
11 eqid lub K = lub K
12 7 10 11 lubel K CLat p X X Base K p K lub K X
13 4 5 9 12 syl3anc K HL X A p A p X p K lub K X
14 13 ex K HL X A p A p X p K lub K X
15 14 ss2rabdv K HL X A p A | p X p A | p K lub K X
16 sseqin2 X A A X = X
17 16 biimpi X A A X = X
18 17 adantl K HL X A A X = X
19 dfin5 A X = p A | p X
20 18 19 eqtr3di K HL X A X = p A | p X
21 eqid pmap K = pmap K
22 11 1 21 2 2polvalN K HL X A ˙ ˙ X = pmap K lub K X
23 sstr X A A Base K X Base K
24 8 23 mpan2 X A X Base K
25 7 11 clatlubcl K CLat X Base K lub K X Base K
26 3 24 25 syl2an K HL X A lub K X Base K
27 7 10 1 21 pmapval K HL lub K X Base K pmap K lub K X = p A | p K lub K X
28 26 27 syldan K HL X A pmap K lub K X = p A | p K lub K X
29 22 28 eqtrd K HL X A ˙ ˙ X = p A | p K lub K X
30 15 20 29 3sstr4d K HL X A X ˙ ˙ X