Theorem somincom

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

	Ref	Expression
Assertion	somincom	⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = if ( 𝐵 𝑅 𝐴 , 𝐵 , 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		so2nr	⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ¬ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) )
2		nan	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ¬ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) ) ↔ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 𝐵 ) → ¬ 𝐵 𝑅 𝐴 ) )
3	1 2	mpbi	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 𝐵 ) → ¬ 𝐵 𝑅 𝐴 )
4	3	iffalsed	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 𝐵 ) → if ( 𝐵 𝑅 𝐴 , 𝐵 , 𝐴 ) = 𝐴 )
5	4	eqcomd	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 𝐵 ) → 𝐴 = if ( 𝐵 𝑅 𝐴 , 𝐵 , 𝐴 ) )
6		sotric	⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝑅 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 𝑅 𝐴 ) ) )
7	6	con2bid	⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 = 𝐵 ∨ 𝐵 𝑅 𝐴 ) ↔ ¬ 𝐴 𝑅 𝐵 ) )
8		ifeq2	⊢ ( 𝐴 = 𝐵 → if ( 𝐵 𝑅 𝐴 , 𝐵 , 𝐴 ) = if ( 𝐵 𝑅 𝐴 , 𝐵 , 𝐵 ) )
9		ifid	⊢ if ( 𝐵 𝑅 𝐴 , 𝐵 , 𝐵 ) = 𝐵
10	8 9	eqtr2di	⊢ ( 𝐴 = 𝐵 → 𝐵 = if ( 𝐵 𝑅 𝐴 , 𝐵 , 𝐴 ) )
11		iftrue	⊢ ( 𝐵 𝑅 𝐴 → if ( 𝐵 𝑅 𝐴 , 𝐵 , 𝐴 ) = 𝐵 )
12	11	eqcomd	⊢ ( 𝐵 𝑅 𝐴 → 𝐵 = if ( 𝐵 𝑅 𝐴 , 𝐵 , 𝐴 ) )
13	10 12	jaoi	⊢ ( ( 𝐴 = 𝐵 ∨ 𝐵 𝑅 𝐴 ) → 𝐵 = if ( 𝐵 𝑅 𝐴 , 𝐵 , 𝐴 ) )
14	7 13	syl6bir	⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ¬ 𝐴 𝑅 𝐵 → 𝐵 = if ( 𝐵 𝑅 𝐴 , 𝐵 , 𝐴 ) ) )
15	14	imp	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ¬ 𝐴 𝑅 𝐵 ) → 𝐵 = if ( 𝐵 𝑅 𝐴 , 𝐵 , 𝐴 ) )
16	5 15	ifeqda	⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = if ( 𝐵 𝑅 𝐴 , 𝐵 , 𝐴 ) )