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

Metamath Proof Explorer

Theorem somin2

Description: Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion somin2 ⊢ R Or X ∧ A ∈ X ∧ B ∈ X → if A R B A B R ∪ I B

Proof

Step Hyp Ref Expression
1 somincom ⊢ R Or X ∧ A ∈ X ∧ B ∈ X → if A R B A B = if B R A B A
2 somin1 ⊢ R Or X ∧ B ∈ X ∧ A ∈ X → if B R A B A R ∪ I B
3 2 ancom2s ⊢ R Or X ∧ A ∈ X ∧ B ∈ X → if B R A B A R ∪ I B
4 1 3 eqbrtrd ⊢ R Or X ∧ A ∈ X ∧ B ∈ X → if A R B A B R ∪ I B