Metamath Proof Explorer

Theorem 2polcon4bN

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

Ref Expression
Hypotheses 2polss.a 
|- A = ( Atoms ` K )
2polss.p 
|- ._|_ = ( _|_P ` K )
Assertion 2polcon4bN 
|- ( ( K e. HL /\ X C_ A /\ 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 simpl1 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) C_ ( ._|_ ` ( ._|_ ` Y ) ) ) -> K e. HL )
4 simp1 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> K e. HL )
5 1 2 polssatN 
 |-  ( ( K e. HL /\ Y C_ A ) -> ( ._|_ ` Y ) C_ A )
6 5 3adant2 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ._|_ ` Y ) C_ A )
7 1 2 polssatN 
 |-  ( ( K e. HL /\ ( ._|_ ` Y ) C_ A ) -> ( ._|_ ` ( ._|_ ` Y ) ) C_ A )
8 4 6 7 syl2anc 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ._|_ ` ( ._|_ ` Y ) ) C_ A )
9 8 adantr 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) C_ ( ._|_ ` ( ._|_ ` Y ) ) ) -> ( ._|_ ` ( ._|_ ` Y ) ) C_ A )
10 simpr 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) C_ ( ._|_ ` ( ._|_ ` Y ) ) ) -> ( ._|_ ` ( ._|_ ` X ) ) C_ ( ._|_ ` ( ._|_ ` Y ) ) )
11 1 2 polcon3N 
 |-  ( ( K e. HL /\ ( ._|_ ` ( ._|_ ` Y ) ) C_ A /\ ( ._|_ ` ( ._|_ ` X ) ) C_ ( ._|_ ` ( ._|_ ` Y ) ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` Y ) ) ) C_ ( ._|_ ` ( ._|_ ` ( ._|_ ` X ) ) ) )
12 3 9 10 11 syl3anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) C_ ( ._|_ ` ( ._|_ ` Y ) ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` Y ) ) ) C_ ( ._|_ ` ( ._|_ ` ( ._|_ ` X ) ) ) )
13 12 ex 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ( ._|_ ` ( ._|_ ` X ) ) C_ ( ._|_ ` ( ._|_ ` Y ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` Y ) ) ) C_ ( ._|_ ` ( ._|_ ` ( ._|_ ` X ) ) ) ) )
14 1 2 3polN 
 |-  ( ( K e. HL /\ Y C_ A ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` Y ) ) ) = ( ._|_ ` Y ) )
15 14 3adant2 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` Y ) ) ) = ( ._|_ ` Y ) )
16 1 2 3polN 
 |-  ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` X ) ) ) = ( ._|_ ` X ) )
17 16 3adant3 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` X ) ) ) = ( ._|_ ` X ) )
18 15 17 sseq12d 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ( ._|_ ` ( ._|_ ` ( ._|_ ` Y ) ) ) C_ ( ._|_ ` ( ._|_ ` ( ._|_ ` X ) ) ) <-> ( ._|_ ` Y ) C_ ( ._|_ ` X ) ) )
19 13 18 sylibd 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ( ._|_ ` ( ._|_ ` X ) ) C_ ( ._|_ ` ( ._|_ ` Y ) ) -> ( ._|_ ` Y ) C_ ( ._|_ ` X ) ) )
20 simpl1 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( ._|_ ` Y ) C_ ( ._|_ ` X ) ) -> K e. HL )
21 1 2 polssatN 
 |-  ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) C_ A )
22 21 3adant3 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ._|_ ` X ) C_ A )
23 22 adantr 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( ._|_ ` Y ) C_ ( ._|_ ` X ) ) -> ( ._|_ ` X ) C_ A )
24 simpr 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( ._|_ ` Y ) C_ ( ._|_ ` X ) ) -> ( ._|_ ` Y ) C_ ( ._|_ ` X ) )
25 1 2 polcon3N 
 |-  ( ( K e. HL /\ ( ._|_ ` X ) C_ A /\ ( ._|_ ` Y ) C_ ( ._|_ ` X ) ) -> ( ._|_ ` ( ._|_ ` X ) ) C_ ( ._|_ ` ( ._|_ ` Y ) ) )
26 20 23 24 25 syl3anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( ._|_ ` Y ) C_ ( ._|_ ` X ) ) -> ( ._|_ ` ( ._|_ ` X ) ) C_ ( ._|_ ` ( ._|_ ` Y ) ) )
27 26 ex 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ( ._|_ ` Y ) C_ ( ._|_ ` X ) -> ( ._|_ ` ( ._|_ ` X ) ) C_ ( ._|_ ` ( ._|_ ` Y ) ) ) )
28 19 27 impbid 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ( ._|_ ` ( ._|_ ` X ) ) C_ ( ._|_ ` ( ._|_ ` Y ) ) <-> ( ._|_ ` Y ) C_ ( ._|_ ` X ) ) )