Theorem en1b

Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015) Avoid ax-un . (Revised by BTernaryTau, 24-Sep-2024)

	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		unisnv	$$⊢\bigcup \left\{x\right\}=x$$
5	3 4	eqtrdi	$$⊢A=\left\{x\right\}\to \bigcup A=x$$
6	5	sneqd	$$⊢A=\left\{x\right\}\to \left\{\bigcup A\right\}=\left\{x\right\}$$
7	2 6	eqtr4d	$$⊢A=\left\{x\right\}\to A=\left\{\bigcup A\right\}$$
8	7	exlimiv	$$⊢\exists xA=\left\{x\right\}\to A=\left\{\bigcup A\right\}$$
9	1 8	sylbi	$$⊢A\approx 1_{𝑜}\to A=\left\{\bigcup A\right\}$$
10		id	$$⊢A=\left\{\bigcup A\right\}\to A=\left\{\bigcup A\right\}$$
11		eqsnuniex	$$⊢A=\left\{\bigcup A\right\}\to \bigcup A\in \mathrm{V}$$
12		ensn1g	$$⊢\bigcup A\in \mathrm{V}\to \left\{\bigcup A\right\}\approx 1_{𝑜}$$
13	11 12	syl	$$⊢A=\left\{\bigcup A\right\}\to \left\{\bigcup A\right\}\approx 1_{𝑜}$$
14	10 13	eqbrtrd	$$⊢A=\left\{\bigcup A\right\}\to A\approx 1_{𝑜}$$
15	9 14	impbii	$$⊢A\approx 1_{𝑜}\leftrightarrow A=\left\{\bigcup A\right\}$$