Theorem en1b

Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015)

	Ref	Expression
Assertion	en1b	$$⊢A\approx 1_{𝑜}\leftrightarrow A=\left\{\bigcup A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		en1	$$⊢A\approx 1_{𝑜}\leftrightarrow \exists xA=\left\{x\right\}$$
2		id	$$⊢A=\left\{x\right\}\to A=\left\{x\right\}$$
3		unieq	$$⊢A=\left\{x\right\}\to \bigcup A=\bigcup \left\{x\right\}$$
4		vex	$$⊢x\in \mathrm{V}$$
5	4	unisn	$$⊢\bigcup \left\{x\right\}=x$$
6	3 5	eqtrdi	$$⊢A=\left\{x\right\}\to \bigcup A=x$$
7	6	sneqd	$$⊢A=\left\{x\right\}\to \left\{\bigcup A\right\}=\left\{x\right\}$$
8	2 7	eqtr4d	$$⊢A=\left\{x\right\}\to A=\left\{\bigcup A\right\}$$
9	8	exlimiv	$$⊢\exists xA=\left\{x\right\}\to A=\left\{\bigcup A\right\}$$
10	1 9	sylbi	$$⊢A\approx 1_{𝑜}\to A=\left\{\bigcup A\right\}$$
11		id	$$⊢A=\left\{\bigcup A\right\}\to A=\left\{\bigcup A\right\}$$
12		snex	$$⊢\left\{\bigcup A\right\}\in \mathrm{V}$$
13	11 12	eqeltrdi	$$⊢A=\left\{\bigcup A\right\}\to A\in \mathrm{V}$$
14	13	uniexd	$$⊢A=\left\{\bigcup A\right\}\to \bigcup A\in \mathrm{V}$$
15		ensn1g	$$⊢\bigcup A\in \mathrm{V}\to \left\{\bigcup A\right\}\approx 1_{𝑜}$$
16	14 15	syl	$$⊢A=\left\{\bigcup A\right\}\to \left\{\bigcup A\right\}\approx 1_{𝑜}$$
17	11 16	eqbrtrd	$$⊢A=\left\{\bigcup A\right\}\to A\approx 1_{𝑜}$$
18	10 17	impbii	$$⊢A\approx 1_{𝑜}\leftrightarrow A=\left\{\bigcup A\right\}$$