This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem df2o3

Description: Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015)

		Ref	Expression
	Assertion	df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$

Step	Hyp	Ref	Expression
1		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
2		df-suc	$⊢ suc 1_{𝑜} = 1_{𝑜} \cup \{1_{𝑜}\}$
3		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
4	3	uneq1i	$⊢ 1_{𝑜} \cup \{1_{𝑜}\} = \{\emptyset\} \cup \{1_{𝑜}\}$
5		df-pr	$⊢ \{\emptyset, 1_{𝑜}\} = \{\emptyset\} \cup \{1_{𝑜}\}$
6	4 5	eqtr4i	$⊢ 1_{𝑜} \cup \{1_{𝑜}\} = \{\emptyset, 1_{𝑜}\}$
7	1 2 6	3eqtri	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$