This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem polcon2N

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

Ref Expression
Hypotheses 2polss.a 
|- A = ( Atoms ` K )
2polss.p 
|- ._|_ = ( _|_P ` K )
Assertion polcon2N 
|- ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> Y C_ ( ._|_ ` X ) )

Proof

Step Hyp Ref Expression
1 2polss.a 
 |-  A = ( Atoms ` K )
2 2polss.p 
 |-  ._|_ = ( _|_P ` K )
3 1 2 2polssN 
 |-  ( ( K e. HL /\ Y C_ A ) -> Y C_ ( ._|_ ` ( ._|_ ` Y ) ) )
4 3 3adant3 
 |-  ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> Y C_ ( ._|_ ` ( ._|_ ` Y ) ) )
5 1 2 polssatN 
 |-  ( ( K e. HL /\ Y C_ A ) -> ( ._|_ ` Y ) C_ A )
6 5 3adant3 
 |-  ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> ( ._|_ ` Y ) C_ A )
7 1 2 polcon3N 
 |-  ( ( K e. HL /\ ( ._|_ ` Y ) C_ A /\ X C_ ( ._|_ ` Y ) ) -> ( ._|_ ` ( ._|_ ` Y ) ) C_ ( ._|_ ` X ) )
8 6 7 syld3an2 
 |-  ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> ( ._|_ ` ( ._|_ ` Y ) ) C_ ( ._|_ ` X ) )
9 4 8 sstrd 
 |-  ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> Y C_ ( ._|_ ` X ) )