Metamath Proof Explorer


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