Theorem df3o3

Description: Ordinal 3, fully expanded. (Contributed by RP, 8-Jul-2021)

	Ref	Expression
Assertion	df3o3	$$⊢3_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\},\left\{\varnothing ,\left\{\varnothing \right\}\right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-3o	$$⊢3_{𝑜}=\mathrm{suc}{2}_{𝑜}$$
2		df2o2	$$⊢2_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
3	2	sneqi	$$⊢\left\{2_{𝑜}\right\}=\left\{\left\{\varnothing ,\left\{\varnothing \right\}\right\}\right\}$$
4	2 3	uneq12i	$$⊢2_{𝑜}\cup \left\{2_{𝑜}\right\}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}\cup \left\{\left\{\varnothing ,\left\{\varnothing \right\}\right\}\right\}$$
5		df-suc	$$⊢\mathrm{suc}{2}_{𝑜}=2_{𝑜}\cup \left\{2_{𝑜}\right\}$$
6		df-tp	$$⊢\left\{\varnothing ,\left\{\varnothing \right\},\left\{\varnothing ,\left\{\varnothing \right\}\right\}\right\}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}\cup \left\{\left\{\varnothing ,\left\{\varnothing \right\}\right\}\right\}$$
7	4 5 6	3eqtr4i	$$⊢\mathrm{suc}{2}_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\},\left\{\varnothing ,\left\{\varnothing \right\}\right\}\right\}$$
8	1 7	eqtri	$$⊢3_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\},\left\{\varnothing ,\left\{\varnothing \right\}\right\}\right\}$$