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	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	2polss.p	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
Assertion	2polssN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		2polss.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		2polss.p	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
3		hlclat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
4	3	ad3antrrr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ∈ 𝑋 ) → 𝐾 ∈ CLat )
5		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ∈ 𝑋 ) → 𝑝 ∈ 𝑋 )
6		simpllr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ∈ 𝑋 ) → 𝑋 ⊆ 𝐴 )
7		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8	7 1	atssbase	⊢ 𝐴 ⊆ ( Base ‘ 𝐾 )
9	6 8	sstrdi	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ∈ 𝑋 ) → 𝑋 ⊆ ( Base ‘ 𝐾 ) )
10		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
11		eqid	⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
12	7 10 11	lubel	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑝 ∈ 𝑋 ∧ 𝑋 ⊆ ( Base ‘ 𝐾 ) ) → 𝑝 ( le ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) )
13	4 5 9 12	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ∈ 𝑋 ) → 𝑝 ( le ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) )
14	13	ex	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 ∈ 𝑋 → 𝑝 ( le ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) )
15	14	ss2rabdv	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → { 𝑝 ∈ 𝐴 ∣ 𝑝 ∈ 𝑋 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ( le ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) } )
16		dfin5	⊢ ( 𝐴 ∩ 𝑋 ) = { 𝑝 ∈ 𝐴 ∣ 𝑝 ∈ 𝑋 }
17		sseqin2	⊢ ( 𝑋 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝑋 ) = 𝑋 )
18	17	biimpi	⊢ ( 𝑋 ⊆ 𝐴 → ( 𝐴 ∩ 𝑋 ) = 𝑋 )
19	18	adantl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐴 ∩ 𝑋 ) = 𝑋 )
20	16 19	syl5reqr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ∈ 𝑋 } )
21		eqid	⊢ ( pmap ‘ 𝐾 ) = ( pmap ‘ 𝐾 )
22	11 1 21 2	2polvalN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) )
23		sstr	⊢ ( ( 𝑋 ⊆ 𝐴 ∧ 𝐴 ⊆ ( Base ‘ 𝐾 ) ) → 𝑋 ⊆ ( Base ‘ 𝐾 ) )
24	8 23	mpan2	⊢ ( 𝑋 ⊆ 𝐴 → 𝑋 ⊆ ( Base ‘ 𝐾 ) )
25	7 11	clatlubcl	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑋 ⊆ ( Base ‘ 𝐾 ) ) → ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
26	3 24 25	syl2an	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
27	7 10 1 21	pmapval	⊢ ( ( 𝐾 ∈ HL ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) = { 𝑝 ∈ 𝐴 ∣ 𝑝 ( le ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) } )
28	26 27	syldan	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) = { 𝑝 ∈ 𝐴 ∣ 𝑝 ( le ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) } )
29	22 28	eqtrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = { 𝑝 ∈ 𝐴 ∣ 𝑝 ( le ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) } )
30	15 20 29	3sstr4d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )