Theorem opcon1b

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

	Ref	Expression
Hypotheses	opoccl.b	|- B = ( Base ` K )
	opoccl.o	|- ._|_ = ( oc ` K )
Assertion	opcon1b	|- ( ( 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	opcon2b	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X = ( ._|_ ` Y ) <-> Y = ( ._|_ ` X ) ) )
4		eqcom	|- ( ( ._|_ ` Y ) = X <-> X = ( ._|_ ` Y ) )
5		eqcom	|- ( ( ._|_ ` X ) = Y <-> Y = ( ._|_ ` X ) )
6	3 4 5	3bitr4g	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` Y ) = X <-> ( ._|_ ` X ) = Y ) )
7	6	bicomd	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) = Y <-> ( ._|_ ` Y ) = X ) )