Theorem df3o2

Description: Ordinal 3 is the unordered triple containing ordinals 0, 1, and 2. (Contributed by RP, 8-Jul-2021)

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

Proof

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