Theorem en4

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

	Ref	Expression
Assertion	en4	$$⊢A\approx 4_{𝑜}\to \exists x\exists y\exists z\exists wA=\left\{x,y\right\}\cup \left\{z,w\right\}$$

Proof

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