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

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

Metamath Proof Explorer