Theorem so0

Description: Any relation is a strict ordering of the empty set. (Contributed by NM, 16-Mar-1997) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	so0	$$⊢R\mathrm{Or}\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		po0	$$⊢R\mathrm{Po}\varnothing$$
2		ral0	$$⊢\forall x\in \varnothing \forall y\in \varnothing \left(xRy\vee x=y\vee yRx\right)$$
3		df-so	$$⊢R\mathrm{Or}\varnothing \leftrightarrow \left(R\mathrm{Po}\varnothing \wedge \forall x\in \varnothing \forall y\in \varnothing \left(xRy\vee x=y\vee yRx\right)\right)$$
4	1 2 3	mpbir2an	$$⊢R\mathrm{Or}\varnothing$$