somincom

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

		Ref	Expression
	Assertion	somincom	$⊢ (R Or X \land (A \in X \land B \in X)) \to if (A R B, A, B) = if (B R A, B, A)$

Step	Hyp	Ref	Expression
1		so2nr	$⊢ (R Or X \land (A \in X \land B \in X)) \to \neg (A R B \land B R A)$
2		nan	$⊢ ((R Or X \land (A \in X \land B \in X)) \to \neg (A R B \land B R A)) \leftrightarrow (((R Or X \land (A \in X \land B \in X)) \land A R B) \to \neg B R A)$
3	1 2	mpbi	$⊢ ((R Or X \land (A \in X \land B \in X)) \land A R B) \to \neg B R A$
4	3	iffalsed	$⊢ ((R Or X \land (A \in X \land B \in X)) \land A R B) \to if (B R A, B, A) = A$
5	4	eqcomd	$⊢ ((R Or X \land (A \in X \land B \in X)) \land A R B) \to A = if (B R A, B, A)$
6		sotric	$⊢ (R Or X \land (A \in X \land B \in X)) \to (A R B \leftrightarrow \neg (A = B \lor B R A))$
7	6	con2bid	$⊢ (R Or X \land (A \in X \land B \in X)) \to ((A = B \lor B R A) \leftrightarrow \neg A R B)$
8		ifeq2	$⊢ A = B \to 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 \to B = if (B R A, B, A)$
11		iftrue	$⊢ B R A \to if (B R A, B, A) = B$
12	11	eqcomd	$⊢ B R A \to B = if (B R A, B, A)$
13	10 12	jaoi	$⊢ (A = B \lor B R A) \to B = if (B R A, B, A)$
14	7 13	syl6bir	$⊢ (R Or X \land (A \in X \land B \in X)) \to (\neg A R B \to B = if (B R A, B, A))$
15	14	imp	$⊢ ((R Or X \land (A \in X \land B \in X)) \land \neg A R B) \to B = if (B R A, B, A)$
16	5 15	ifeqda	$⊢ (R Or X \land (A \in X \land B \in X)) \to if (A R B, A, B) = if (B R A, B, A)$

Metamath Proof Explorer