0we1

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

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

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

Metamath Proof Explorer