Theorem en3

Description: A set equinumerous to ordinal 3 is a triple. (Contributed by Mario Carneiro, 5-Jan-2016)

	Ref	Expression
Assertion	en3	$$⊢A\approx 3_{𝑜}\to \exists x\exists y\exists zA=\left\{x,y,z\right\}$$

Proof

Step	Hyp	Ref	Expression
1		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
2	1	onordi	$$⊢\mathrm{Ord}{2}_{𝑜}$$
3		df-3o	$$⊢3_{𝑜}=\mathrm{suc}{2}_{𝑜}$$
4		en2	$$⊢\left(A\setminus \left\{x\right\}\right)\approx 2_{𝑜}\to \exists y\exists zA\setminus \left\{x\right\}=\left\{y,z\right\}$$
5		tpass	$$⊢\left\{x,y,z\right\}=\left\{x\right\}\cup \left\{y,z\right\}$$
6	5	enp1ilem	$$⊢x\in A\to \left(A\setminus \left\{x\right\}=\left\{y,z\right\}\to A=\left\{x,y,z\right\}\right)$$
7	6	2eximdv	$$⊢x\in A\to \left(\exists y\exists zA\setminus \left\{x\right\}=\left\{y,z\right\}\to \exists y\exists zA=\left\{x,y,z\right\}\right)$$
8	2 3 4 7	enp1i	$$⊢A\approx 3_{𝑜}\to \exists x\exists y\exists zA=\left\{x,y,z\right\}$$