Metamath Proof Explorer

Theorem somincom

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

Ref Expression
Assertion somincom ⊢ R Or X ∧ A ∈ X ∧ B ∈ X → if A R B A B = if B R A B A

Proof

Step Hyp Ref Expression
1 so2nr ⊢ R Or X ∧ A ∈ X ∧ B ∈ X → ¬ A R B ∧ B R A
2 nan ⊢ R Or X ∧ A ∈ X ∧ B ∈ X → ¬ A R B ∧ B R A ↔ R Or X ∧ A ∈ X ∧ B ∈ X ∧ A R B → ¬ B R A
3 1 2 mpbi ⊢ R Or X ∧ A ∈ X ∧ B ∈ X ∧ A R B → ¬ B R A
4 3 iffalsed ⊢ R Or X ∧ A ∈ X ∧ B ∈ X ∧ A R B → if B R A B A = A
5 4 eqcomd ⊢ R Or X ∧ A ∈ X ∧ B ∈ X ∧ A R B → A = if B R A B A
6 sotric ⊢ R Or X ∧ A ∈ X ∧ B ∈ X → A R B ↔ ¬ A = B ∨ B R A
7 6 con2bid ⊢ R Or X ∧ A ∈ X ∧ B ∈ X → A = B ∨ B R A ↔ ¬ A R B
8 ifeq2 ⊢ A = B → if B R A B A = if B R A B B
9 ifid ⊢ if B R A B B = B
10 8 9 syl6req ⊢ A = B → B = if B R A B A
11 iftrue ⊢ B R A → if B R A B A = B
12 11 eqcomd ⊢ B R A → B = if B R A B A
13 10 12 jaoi ⊢ A = B ∨ B R A → B = if B R A B A
14 7 13 syl6bir ⊢ R Or X ∧ A ∈ X ∧ B ∈ X → ¬ A R B → B = if B R A B A
15 14 imp ⊢ R Or X ∧ A ∈ X ∧ B ∈ X ∧ ¬ A R B → B = if B R A B A
16 5 15 ifeqda ⊢ R Or X ∧ A ∈ X ∧ B ∈ X → if A R B A B = if B R A B A