Metamath Proof Explorer

Theorem poleloe

Description: Express "less than or equals" for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion poleloe 
|- ( B e. V -> ( A ( R u. _I ) B <-> ( A R B \/ A = B ) ) )

Proof

Step Hyp Ref Expression
1 brun 
 |-  ( A ( R u. _I ) B <-> ( A R B \/ A _I B ) )
2 ideqg 
 |-  ( B e. V -> ( A _I B <-> A = B ) )
3 2 orbi2d 
 |-  ( B e. V -> ( ( A R B \/ A _I B ) <-> ( A R B \/ A = B ) ) )
4 1 3 bitrid 
 |-  ( B e. V -> ( A ( R u. _I ) B <-> ( A R B \/ A = B ) ) )