ensn1

Description: A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002) Avoid ax-un . (Revised by BTernaryTau, 23-Sep-2024)

		Ref	Expression
	Hypothesis	ensn1.1	$⊢ A \in V$
	Assertion	ensn1	$⊢ \{A\} \approx 1_{𝑜}$

Step	Hyp	Ref	Expression
1		ensn1.1	$⊢ A \in V$
2		snex	$⊢ \{⟨A, \emptyset⟩\} \in V$
3		f1oeq1	$⊢ f = \{⟨A, \emptyset⟩\} \to (f : \{A\} \underset{1-1 onto}{⟶} \{\emptyset\} \leftrightarrow \{⟨A, \emptyset⟩\} : \{A\} \underset{1-1 onto}{⟶} \{\emptyset\})$
4		0ex	$⊢ \emptyset \in V$
5	1 4	f1osn	$⊢ \{⟨A, \emptyset⟩\} : \{A\} \underset{1-1 onto}{⟶} \{\emptyset\}$
6	2 3 5	ceqsexv2d	$⊢ \exists f f : \{A\} \underset{1-1 onto}{⟶} \{\emptyset\}$
7		snex	$⊢ \{A\} \in V$
8		snex	$⊢ \{\emptyset\} \in V$
9		breng	$⊢ (\{A\} \in V \land \{\emptyset\} \in V) \to (\{A\} \approx \{\emptyset\} \leftrightarrow \exists f f : \{A\} \underset{1-1 onto}{⟶} \{\emptyset\})$
10	7 8 9	mp2an	$⊢ \{A\} \approx \{\emptyset\} \leftrightarrow \exists f f : \{A\} \underset{1-1 onto}{⟶} \{\emptyset\}$
11	6 10	mpbir	$⊢ \{A\} \approx \{\emptyset\}$
12		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
13	11 12	breqtrri	$⊢ \{A\} \approx 1_{𝑜}$

Metamath Proof Explorer