Theorem opcon2b

Description: Orthocomplement contraposition law. ( negcon2 analog.) (Contributed by NM, 16-Jan-2012)

	Ref	Expression
Hypotheses	opoccl.b	|- B = ( Base ` K )
	opoccl.o	|- ._|_ = ( oc ` K )
Assertion	opcon2b	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X = ( ._|_ ` Y ) <-> Y = ( ._|_ ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		opoccl.b	|- B = ( Base ` K )
2		opoccl.o	|- ._|_ = ( oc ` K )
3	1 2	opoccl	|- ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
4	3	3adant2	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
5	1 2	opcon3b	|- ( ( K e. OP /\ X e. B /\ ( ._|_ ` Y ) e. B ) -> ( X = ( ._|_ ` Y ) <-> ( ._|_ ` ( ._|_ ` Y ) ) = ( ._|_ ` X ) ) )
6	4 5	syld3an3	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X = ( ._|_ ` Y ) <-> ( ._|_ ` ( ._|_ ` Y ) ) = ( ._|_ ` X ) ) )
7	1 2	opococ	|- ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y )
8	7	3adant2	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y )
9	8	eqeq1d	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` ( ._|_ ` Y ) ) = ( ._|_ ` X ) <-> Y = ( ._|_ ` X ) ) )
10	6 9	bitrd	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X = ( ._|_ ` Y ) <-> Y = ( ._|_ ` X ) ) )