Theorem somin2

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

	Ref	Expression
Assertion	somin2	⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) ( 𝑅 ∪ I ) 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		somincom	⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = if ( 𝐵 𝑅 𝐴 , 𝐵 , 𝐴 ) )
2		somin1	⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → if ( 𝐵 𝑅 𝐴 , 𝐵 , 𝐴 ) ( 𝑅 ∪ I ) 𝐵 )
3	2	ancom2s	⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → if ( 𝐵 𝑅 𝐴 , 𝐵 , 𝐴 ) ( 𝑅 ∪ I ) 𝐵 )
4	1 3	eqbrtrd	⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) ( 𝑅 ∪ I ) 𝐵 )