Metamath Proof Explorer


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