Theorem opcon3b

Description: Contraposition law for orthoposets. ( chcon3i analog.) (Contributed by NM, 8-Nov-2011)

	Ref	Expression
Hypotheses	opoccl.b	|- B = ( Base ` K )
	opoccl.o	|- ._|_ = ( oc ` K )
Assertion	opcon3b	|- ( ( 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		fveq2	|- ( Y = X -> ( ._|_ ` Y ) = ( ._|_ ` X ) )
4	3	eqcoms	|- ( X = Y -> ( ._|_ ` Y ) = ( ._|_ ` X ) )
5		fveq2	|- ( ( ._|_ ` X ) = ( ._|_ ` Y ) -> ( ._|_ ` ( ._|_ ` X ) ) = ( ._|_ ` ( ._|_ ` Y ) ) )
6	5	eqcoms	|- ( ( ._|_ ` Y ) = ( ._|_ ` X ) -> ( ._|_ ` ( ._|_ ` X ) ) = ( ._|_ ` ( ._|_ ` Y ) ) )
7	1 2	opococ	|- ( ( K e. OP /\ X e. B ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
8	7	3adant3	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
9	1 2	opococ	|- ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y )
10	9	3adant2	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y )
11	8 10	eqeq12d	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` ( ._|_ ` X ) ) = ( ._|_ ` ( ._|_ ` Y ) ) <-> X = Y ) )
12	6 11	syl5ib	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` Y ) = ( ._|_ ` X ) -> X = Y ) )
13	4 12	impbid2	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X = Y <-> ( ._|_ ` Y ) = ( ._|_ ` X ) ) )