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 𝐴 = ( 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 biimpi ( 𝑋𝐴 → ( 𝐴𝑋 ) = 𝑋 )
18 17 adantl ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) → ( 𝐴𝑋 ) = 𝑋 )
19 dfin5 ( 𝐴𝑋 ) = { 𝑝𝐴𝑝𝑋 }
20 18 19 eqtr3di ( ( 𝐾 ∈ 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 ∧ 𝑋𝐴 ) → 𝑋 ⊆ ( ‘ ( 𝑋 ) ) )