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 ) )