Theorem somin2

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

	Ref	Expression
Assertion	somin2	$$⊢\left(R\mathrm{Or}X\wedge \left(A\in X\wedge B\in X\right)\right)\to if\left(ARB,A,B\right)\left(R\cup \mathrm{I}\right)B$$

Proof

Step	Hyp	Ref	Expression
1		somincom	$$⊢\left(R\mathrm{Or}X\wedge \left(A\in X\wedge B\in X\right)\right)\to if\left(ARB,A,B\right)=if\left(BRA,B,A\right)$$
2		somin1	$$⊢\left(R\mathrm{Or}X\wedge \left(B\in X\wedge A\in X\right)\right)\to if\left(BRA,B,A\right)\left(R\cup \mathrm{I}\right)B$$
3	2	ancom2s	$$⊢\left(R\mathrm{Or}X\wedge \left(A\in X\wedge B\in X\right)\right)\to if\left(BRA,B,A\right)\left(R\cup \mathrm{I}\right)B$$
4	1 3	eqbrtrd	$$⊢\left(R\mathrm{Or}X\wedge \left(A\in X\wedge B\in X\right)\right)\to if\left(ARB,A,B\right)\left(R\cup \mathrm{I}\right)B$$