Theorem 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 \left(\left|A\right|=1\leftrightarrow A\approx 1_{𝑜}\right)$$

Proof

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