card1

Description: A set has cardinality one iff it is a singleton. (Contributed by Mario Carneiro, 10-Jan-2013)

		Ref	Expression
	Assertion	card1	$⊢ card (A) = 1_{𝑜} \leftrightarrow \exists x A = \{x\}$

Step	Hyp	Ref	Expression
1		1onn	$⊢ 1_{𝑜} \in ω$
2		cardnn	$⊢ 1_{𝑜} \in ω \to card (1_{𝑜}) = 1_{𝑜}$
3	1 2	ax-mp	$⊢ card (1_{𝑜}) = 1_{𝑜}$
4		1n0	$⊢ 1_{𝑜} \neq \emptyset$
5	3 4	eqnetri	$⊢ card (1_{𝑜}) \neq \emptyset$
6		carden2a	$⊢ (card (1_{𝑜}) = card (A) \land card (1_{𝑜}) \neq \emptyset) \to 1_{𝑜} \approx A$
7	5 6	mpan2	$⊢ card (1_{𝑜}) = card (A) \to 1_{𝑜} \approx A$
8	7	eqcoms	$⊢ card (A) = card (1_{𝑜}) \to 1_{𝑜} \approx A$
9	8	ensymd	$⊢ card (A) = card (1_{𝑜}) \to A \approx 1_{𝑜}$
10		carden2b	$⊢ A \approx 1_{𝑜} \to card (A) = card (1_{𝑜})$
11	9 10	impbii	$⊢ card (A) = card (1_{𝑜}) \leftrightarrow A \approx 1_{𝑜}$
12	3	eqeq2i	$⊢ card (A) = card (1_{𝑜}) \leftrightarrow card (A) = 1_{𝑜}$
13		en1	$⊢ A \approx 1_{𝑜} \leftrightarrow \exists x A = \{x\}$
14	11 12 13	3bitr3i	$⊢ card (A) = 1_{𝑜} \leftrightarrow \exists x A = \{x\}$

Metamath Proof Explorer