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 w A = \{x, y\} \cup \{z, w\}$

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

Metamath Proof Explorer