Theorem oplecon3b

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

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

Proof

Step	Hyp	Ref	Expression
1		opcon3.b	|- B = ( Base ` K )
2		opcon3.l	|- .<_ = ( le ` K )
3		opcon3.o	|- ._|_ = ( oc ` K )
4	1 2 3	oplecon3	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) )
5		simp1	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> K e. OP )
6	1 3	opoccl	|- ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
7	6	3adant2	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
8	1 3	opoccl	|- ( ( K e. OP /\ X e. B ) -> ( ._|_ ` X ) e. B )
9	8	3adant3	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ._|_ ` X ) e. B )
10	1 2 3	oplecon3	|- ( ( K e. OP /\ ( ._|_ ` Y ) e. B /\ ( ._|_ ` X ) e. B ) -> ( ( ._|_ ` Y ) .<_ ( ._|_ ` X ) -> ( ._|_ ` ( ._|_ ` X ) ) .<_ ( ._|_ ` ( ._|_ ` Y ) ) ) )
11	5 7 9 10	syl3anc	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` Y ) .<_ ( ._|_ ` X ) -> ( ._|_ ` ( ._|_ ` X ) ) .<_ ( ._|_ ` ( ._|_ ` Y ) ) ) )
12	1 3	opococ	|- ( ( K e. OP /\ X e. B ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
13	12	3adant3	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
14	1 3	opococ	|- ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y )
15	14	3adant2	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y )
16	13 15	breq12d	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` ( ._|_ ` X ) ) .<_ ( ._|_ ` ( ._|_ ` Y ) ) <-> X .<_ Y ) )
17	11 16	sylibd	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` Y ) .<_ ( ._|_ ` X ) -> X .<_ Y ) )
18	4 17	impbid	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) )