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	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
Assertion	2polssN	$⊢ (K \in HL \land X \subseteq A) \to X \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))$

Proof

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

Metamath Proof Explorer

Theorem 2polssN

Proof