Theorem 0we1

Description: The empty set is a well-ordering of ordinal one. (Contributed by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Assertion	0we1	$$⊢\varnothing \mathrm{We}{1}_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		br0	$$⊢\neg \varnothing \varnothing \varnothing$$
2		rel0	$$⊢\mathrm{Rel}\varnothing$$
3		wesn	$$⊢\mathrm{Rel}\varnothing \to \left(\varnothing \mathrm{We}\left\{\varnothing \right\}\leftrightarrow \neg \varnothing \varnothing \varnothing \right)$$
4	2 3	ax-mp	$$⊢\varnothing \mathrm{We}\left\{\varnothing \right\}\leftrightarrow \neg \varnothing \varnothing \varnothing$$
5	1 4	mpbir	$$⊢\varnothing \mathrm{We}\left\{\varnothing \right\}$$
6		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
7		weeq2	$$⊢1_{𝑜}=\left\{\varnothing \right\}\to \left(\varnothing \mathrm{We}{1}_{𝑜}\leftrightarrow \varnothing \mathrm{We}\left\{\varnothing \right\}\right)$$
8	6 7	ax-mp	$$⊢\varnothing \mathrm{We}{1}_{𝑜}\leftrightarrow \varnothing \mathrm{We}\left\{\varnothing \right\}$$
9	5 8	mpbir	$$⊢\varnothing \mathrm{We}{1}_{𝑜}$$