Theorem issod

Description: An irreflexive, transitive, linear relation is a strict ordering. (Contributed by NM, 21-Jan-1996) (Revised by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Hypotheses	issod.1	$$⊢\phi \to R\mathrm{Po}A$$
	issod.2	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in A\right)\right)\to \left(xRy\vee x=y\vee yRx\right)$$
Assertion	issod	$$⊢\phi \to R\mathrm{Or}A$$

Proof

Step	Hyp	Ref	Expression
1		issod.1	$$⊢\phi \to R\mathrm{Po}A$$
2		issod.2	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in A\right)\right)\to \left(xRy\vee x=y\vee yRx\right)$$
3	2	ralrimivva	$$⊢\phi \to \forall x\in A\forall y\in A\left(xRy\vee x=y\vee yRx\right)$$
4		df-so	$$⊢R\mathrm{Or}A\leftrightarrow \left(R\mathrm{Po}A\wedge \forall x\in A\forall y\in A\left(xRy\vee x=y\vee yRx\right)\right)$$
5	1 3 4	sylanbrc	$$⊢\phi \to R\mathrm{Or}A$$