Theorem we0

Description: Any relation is a well-ordering of the empty set. (Contributed by NM, 16-Mar-1997)

	Ref	Expression
Assertion	we0	$$⊢R\mathrm{We}\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		fr0	$$⊢R\mathrm{Fr}\varnothing$$
2		so0	$$⊢R\mathrm{Or}\varnothing$$
3		df-we	$$⊢R\mathrm{We}\varnothing \leftrightarrow \left(R\mathrm{Fr}\varnothing \wedge R\mathrm{Or}\varnothing \right)$$
4	1 2 3	mpbir2an	$$⊢R\mathrm{We}\varnothing$$