hashen1

Description: A set has size 1 if and only if it is equinumerous to the ordinal 1. (Contributed by AV, 14-Apr-2019)

		Ref	Expression
	Assertion	hashen1	$⊢ A \in V \to (\|A\| = 1 \leftrightarrow A \approx 1_{𝑜})$

Proof

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2		hashsng	$⊢ \emptyset \in V \to \|\{\emptyset\}\| = 1$
3	1 2	ax-mp	$⊢ \|\{\emptyset\}\| = 1$
4	3	eqcomi	$⊢ 1 = \|\{\emptyset\}\|$
5	4	a1i	$⊢ A \in V \to 1 = \|\{\emptyset\}\|$
6	5	eqeq2d	$⊢ A \in V \to (\|A\| = 1 \leftrightarrow \|A\| = \|\{\emptyset\}\|)$
7		simpr	$⊢ (A \in V \land \|A\| = \|\{\emptyset\}\|) \to \|A\| = \|\{\emptyset\}\|$
8		1nn0	$⊢ 1 \in ℕ_{0}$
9	3 8	eqeltri	$⊢ \|\{\emptyset\}\| \in ℕ_{0}$
10		hashvnfin	$⊢ (A \in V \land \|\{\emptyset\}\| \in ℕ_{0}) \to (\|A\| = \|\{\emptyset\}\| \to A \in Fin)$
11	9 10	mpan2	$⊢ A \in V \to (\|A\| = \|\{\emptyset\}\| \to A \in Fin)$
12	11	imp	$⊢ (A \in V \land \|A\| = \|\{\emptyset\}\|) \to A \in Fin$
13		snfi	$⊢ \{\emptyset\} \in Fin$
14		hashen	$⊢ (A \in Fin \land \{\emptyset\} \in Fin) \to (\|A\| = \|\{\emptyset\}\| \leftrightarrow A \approx \{\emptyset\})$
15	12 13 14	sylancl	$⊢ (A \in V \land \|A\| = \|\{\emptyset\}\|) \to (\|A\| = \|\{\emptyset\}\| \leftrightarrow A \approx \{\emptyset\})$
16	7 15	mpbid	$⊢ (A \in V \land \|A\| = \|\{\emptyset\}\|) \to A \approx \{\emptyset\}$
17	16	ex	$⊢ A \in V \to (\|A\| = \|\{\emptyset\}\| \to A \approx \{\emptyset\})$
18		hasheni	$⊢ A \approx \{\emptyset\} \to \|A\| = \|\{\emptyset\}\|$
19	17 18	impbid1	$⊢ A \in V \to (\|A\| = \|\{\emptyset\}\| \leftrightarrow A \approx \{\emptyset\})$
20		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
21	20	eqcomi	$⊢ \{\emptyset\} = 1_{𝑜}$
22	21	breq2i	$⊢ A \approx \{\emptyset\} \leftrightarrow A \approx 1_{𝑜}$
23	22	a1i	$⊢ A \in V \to (A \approx \{\emptyset\} \leftrightarrow A \approx 1_{𝑜})$
24	6 19 23	3bitrd	$⊢ A \in V \to (\|A\| = 1 \leftrightarrow A \approx 1_{𝑜})$

Metamath Proof Explorer

Theorem hashen1

Proof