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 dfin5 
 |-  ( A i^i X ) = { p e. A | p e. X }
17 sseqin2 
 |-  ( X C_ A <-> ( A i^i X ) = X )
18 17 biimpi 
 |-  ( X C_ A -> ( A i^i X ) = X )
19 18 adantl 
 |-  ( ( K e. HL /\ X C_ A ) -> ( A i^i X ) = X )
20 16 19 syl5reqr 
 |-  ( ( 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 ) ) )