Metamath Proof Explorer


Theorem polcon3N

Description: Contraposition law for polarity. Remark in Holland95 p. 223. (Contributed by NM, 23-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2polss.a 𝐴 = ( Atoms ‘ 𝐾 )
2polss.p = ( ⊥𝑃𝐾 )
Assertion polcon3N ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋𝑌 ) → ( 𝑌 ) ⊆ ( 𝑋 ) )

Proof

Step Hyp Ref Expression
1 2polss.a 𝐴 = ( Atoms ‘ 𝐾 )
2 2polss.p = ( ⊥𝑃𝐾 )
3 simp3 ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋𝑌 ) → 𝑋𝑌 )
4 iinss1 ( 𝑋𝑌 𝑝𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ⊆ 𝑝𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) )
5 sslin ( 𝑝𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ⊆ 𝑝𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) → ( 𝐴 𝑝𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ⊆ ( 𝐴 𝑝𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) )
6 3 4 5 3syl ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋𝑌 ) → ( 𝐴 𝑝𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ⊆ ( 𝐴 𝑝𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) )
7 eqid ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
8 eqid ( pmap ‘ 𝐾 ) = ( pmap ‘ 𝐾 )
9 7 1 8 2 polvalN ( ( 𝐾 ∈ HL ∧ 𝑌𝐴 ) → ( 𝑌 ) = ( 𝐴 𝑝𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) )
10 9 3adant3 ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋𝑌 ) → ( 𝑌 ) = ( 𝐴 𝑝𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) )
11 simp1 ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋𝑌 ) → 𝐾 ∈ HL )
12 simp2 ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋𝑌 ) → 𝑌𝐴 )
13 3 12 sstrd ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋𝑌 ) → 𝑋𝐴 )
14 7 1 8 2 polvalN ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) → ( 𝑋 ) = ( 𝐴 𝑝𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) )
15 11 13 14 syl2anc ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋𝑌 ) → ( 𝑋 ) = ( 𝐴 𝑝𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) )
16 6 10 15 3sstr4d ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋𝑌 ) → ( 𝑌 ) ⊆ ( 𝑋 ) )