This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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