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