Theorem 0lt1o

Description: Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005)

	Ref	Expression
Assertion	0lt1o	$$⊢\varnothing \in 1_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\varnothing =\varnothing$$
2		el1o	$$⊢\varnothing \in 1_{𝑜}\leftrightarrow \varnothing =\varnothing$$
3	1 2	mpbir	$$⊢\varnothing \in 1_{𝑜}$$