Metamath Proof Explorer

Theorem gt-lt

Description: Simple relationship between < and > . (Contributed by David A. Wheeler, 19-Apr-2015) (New usage is discouraged.)

Ref Expression
Assertion gt-lt 
|- ( ( A e. _V /\ B e. _V ) -> ( A > B <-> B < A ) )

Proof

Step Hyp Ref Expression
1 df-gt 
 |-  > = `' <
2 1 breqi 
 |-  ( A > B <-> A `' < B )
3 brcnvg 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A `' < B <-> B < A ) )
4 2 3 bitrid 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A > B <-> B < A ) )