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
|- ._|_ = ( _|_P ` K )
Assertion 2polssN
|- ( ( K e. HL /\ X C_ A ) -> X C_ ( ._|_ ` ( ._|_ ` X ) ) )

Proof

Step Hyp Ref Expression
1 2polss.a
 |-  A = ( Atoms ` K )
2 2polss.p
 |-  ._|_ = ( _|_P ` K )
3 hlclat
 |-  ( K e. HL -> K e. CLat )
4 3 ad3antrrr
 |-  ( ( ( ( K e. HL /\ X C_ A ) /\ p e. A ) /\ p e. X ) -> K e. CLat )
5 simpr
 |-  ( ( ( ( K e. HL /\ X C_ A ) /\ p e. A ) /\ p e. X ) -> p e. X )
6 simpllr
 |-  ( ( ( ( K e. HL /\ X C_ A ) /\ p e. A ) /\ p e. X ) -> X C_ A )
7 eqid
 |-  ( Base ` K ) = ( Base ` K )
8 7 1 atssbase
 |-  A C_ ( Base ` K )
9 6 8 sstrdi
 |-  ( ( ( ( K e. HL /\ X C_ A ) /\ p e. A ) /\ p e. X ) -> X C_ ( Base ` K ) )
10 eqid
 |-  ( le ` K ) = ( le ` K )
11 eqid
 |-  ( lub ` K ) = ( lub ` K )
12 7 10 11 lubel
 |-  ( ( K e. CLat /\ p e. X /\ X C_ ( Base ` K ) ) -> p ( le ` K ) ( ( lub ` K ) ` X ) )
13 4 5 9 12 syl3anc
 |-  ( ( ( ( K e. HL /\ X C_ A ) /\ p e. A ) /\ p e. X ) -> p ( le ` K ) ( ( lub ` K ) ` X ) )
14 13 ex
 |-  ( ( ( K e. HL /\ X C_ A ) /\ p e. A ) -> ( p e. X -> p ( le ` K ) ( ( lub ` K ) ` X ) ) )
15 14 ss2rabdv
 |-  ( ( K e. HL /\ X C_ A ) -> { p e. A | p e. X } C_ { p e. A | p ( le ` K ) ( ( lub ` K ) ` X ) } )
16 sseqin2
 |-  ( X C_ A <-> ( A i^i X ) = X )
17 16 biimpi
 |-  ( X C_ A -> ( A i^i X ) = X )
18 17 adantl
 |-  ( ( K e. HL /\ X C_ A ) -> ( A i^i X ) = X )
19 dfin5
 |-  ( A i^i X ) = { p e. A | p e. X }
20 18 19 eqtr3di
 |-  ( ( K e. HL /\ X C_ A ) -> X = { p e. A | p e. X } )
21 eqid
 |-  ( pmap ` K ) = ( pmap ` K )
22 11 1 21 2 2polvalN
 |-  ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` ( ._|_ ` X ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` X ) ) )
23 sstr
 |-  ( ( X C_ A /\ A C_ ( Base ` K ) ) -> X C_ ( Base ` K ) )
24 8 23 mpan2
 |-  ( X C_ A -> X C_ ( Base ` K ) )
25 7 11 clatlubcl
 |-  ( ( K e. CLat /\ X C_ ( Base ` K ) ) -> ( ( lub ` K ) ` X ) e. ( Base ` K ) )
26 3 24 25 syl2an
 |-  ( ( K e. HL /\ X C_ A ) -> ( ( lub ` K ) ` X ) e. ( Base ` K ) )
27 7 10 1 21 pmapval
 |-  ( ( K e. HL /\ ( ( lub ` K ) ` X ) e. ( Base ` K ) ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` X ) ) = { p e. A | p ( le ` K ) ( ( lub ` K ) ` X ) } )
28 26 27 syldan
 |-  ( ( K e. HL /\ X C_ A ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` X ) ) = { p e. A | p ( le ` K ) ( ( lub ` K ) ` X ) } )
29 22 28 eqtrd
 |-  ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` ( ._|_ ` X ) ) = { p e. A | p ( le ` K ) ( ( lub ` K ) ` X ) } )
30 15 20 29 3sstr4d
 |-  ( ( K e. HL /\ X C_ A ) -> X C_ ( ._|_ ` ( ._|_ ` X ) ) )