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		sseqin2	⊢ ( 𝑋 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝑋 ) = 𝑋 )
17	16	bilani	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐴 ∩ 𝑋 ) = 𝑋 )
18		dfin5	⊢ ( 𝐴 ∩ 𝑋 ) = { 𝑝 ∈ 𝐴 ∣ 𝑝 ∈ 𝑋 }
19	17 18	eqtr3di	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ∈ 𝑋 } )
20		eqid	⊢ ( pmap ‘ 𝐾 ) = ( pmap ‘ 𝐾 )
21	11 1 20 2	2polvalN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) )
22		sstr	⊢ ( ( 𝑋 ⊆ 𝐴 ∧ 𝐴 ⊆ ( Base ‘ 𝐾 ) ) → 𝑋 ⊆ ( Base ‘ 𝐾 ) )
23	8 22	mpan2	⊢ ( 𝑋 ⊆ 𝐴 → 𝑋 ⊆ ( Base ‘ 𝐾 ) )
24	7 11	clatlubcl	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑋 ⊆ ( Base ‘ 𝐾 ) ) → ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
25	3 23 24	syl2an	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
26	7 10 1 20	pmapval	⊢ ( ( 𝐾 ∈ HL ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) = { 𝑝 ∈ 𝐴 ∣ 𝑝 ( le ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) } )
27	25 26	syldan	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) = { 𝑝 ∈ 𝐴 ∣ 𝑝 ( le ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) } )
28	21 27	eqtrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = { 𝑝 ∈ 𝐴 ∣ 𝑝 ( le ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) } )
29	15 19 28	3sstr4d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )