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 eqtr2di 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