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

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 ∈ V → A R ∪ I B ↔ A R B ∨ A = B

Proof

Step Hyp Ref Expression
1 brun ⊢ A R ∪ I B ↔ A R B ∨ A I B
2 ideqg ⊢ B ∈ V → A I B ↔ A = B
3 2 orbi2d ⊢ B ∈ V → A R B ∨ A I B ↔ A R B ∨ A = B
4 1 3 bitrid ⊢ B ∈ V → A R ∪ I B ↔ A R B ∨ A = B