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 A = Atoms K
2polss.p ˙ = 𝑃 K
Assertion polcon3N K HL Y A X Y ˙ Y ˙ X

Proof

Step Hyp Ref Expression
1 2polss.a A = Atoms K
2 2polss.p ˙ = 𝑃 K
3 simp3 K HL Y A X Y X Y
4 iinss1 X Y p Y pmap K oc K p p X pmap K oc K p
5 sslin p Y pmap K oc K p p X pmap K oc K p A p Y pmap K oc K p A p X pmap K oc K p
6 3 4 5 3syl K HL Y A X Y A p Y pmap K oc K p A p X pmap K oc K p
7 eqid oc K = oc K
8 eqid pmap K = pmap K
9 7 1 8 2 polvalN K HL Y A ˙ Y = A p Y pmap K oc K p
10 9 3adant3 K HL Y A X Y ˙ Y = A p Y pmap K oc K p
11 simp1 K HL Y A X Y K HL
12 simp2 K HL Y A X Y Y A
13 3 12 sstrd K HL Y A X Y X A
14 7 1 8 2 polvalN K HL X A ˙ X = A p X pmap K oc K p
15 11 13 14 syl2anc K HL Y A X Y ˙ X = A p X pmap K oc K p
16 6 10 15 3sstr4d K HL Y A X Y ˙ Y ˙ X