Theorem ord0

Description: The empty set is an ordinal class. Remark 1.5 of Schloeder p. 1. (Contributed by NM, 11-May-1994)

	Ref	Expression
Assertion	ord0	$$⊢\mathrm{Ord}\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		tr0	$$⊢\mathrm{Tr}\varnothing$$
2		we0	$$⊢\mathrm{E}\mathrm{We}\varnothing$$
3		df-ord	$$⊢\mathrm{Ord}\varnothing \leftrightarrow \left(\mathrm{Tr}\varnothing \wedge \mathrm{E}\mathrm{We}\varnothing \right)$$
4	1 2 3	mpbir2an	$$⊢\mathrm{Ord}\varnothing$$