Metamath Proof Explorer

Theorem gte-lte

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

Ref Expression
Assertion gte-lte 
|- ( ( A e. _V /\ B e. _V ) -> ( A >_ B <-> B <_ A ) )

Proof

Step Hyp Ref Expression
1 df-gte 
 |-  >_ = `' <_
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 ) )