Theorem sdom1

Description: A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 12-Dec-2024)

	Ref	Expression
Assertion	sdom1	$$⊢A\prec 1_{𝑜}\leftrightarrow A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
2	1	breq2i	$$⊢A\preccurlyeq 1_{𝑜}\leftrightarrow A\preccurlyeq \left\{\varnothing \right\}$$
3		brdomi	$$⊢A\preccurlyeq \left\{\varnothing \right\}\to \exists ff:A\underset{1-1}{⟶}\left\{\varnothing \right\}$$
4		f1cdmsn	$$⊢\left(f:A\underset{1-1}{⟶}\left\{\varnothing \right\}\wedge A\ne \varnothing \right)\to \exists xA=\left\{x\right\}$$
5		vex	$$⊢x\in \mathrm{V}$$
6	5	ensn1	$$⊢\left\{x\right\}\approx 1_{𝑜}$$
7		breq1	$$⊢A=\left\{x\right\}\to \left(A\approx 1_{𝑜}\leftrightarrow \left\{x\right\}\approx 1_{𝑜}\right)$$
8	6 7	mpbiri	$$⊢A=\left\{x\right\}\to A\approx 1_{𝑜}$$
9	8	exlimiv	$$⊢\exists xA=\left\{x\right\}\to A\approx 1_{𝑜}$$
10	4 9	syl	$$⊢\left(f:A\underset{1-1}{⟶}\left\{\varnothing \right\}\wedge A\ne \varnothing \right)\to A\approx 1_{𝑜}$$
11	10	expcom	$$⊢A\ne \varnothing \to \left(f:A\underset{1-1}{⟶}\left\{\varnothing \right\}\to A\approx 1_{𝑜}\right)$$
12	11	exlimdv	$$⊢A\ne \varnothing \to \left(\exists ff:A\underset{1-1}{⟶}\left\{\varnothing \right\}\to A\approx 1_{𝑜}\right)$$
13	3 12	syl5	$$⊢A\ne \varnothing \to \left(A\preccurlyeq \left\{\varnothing \right\}\to A\approx 1_{𝑜}\right)$$
14	2 13	biimtrid	$$⊢A\ne \varnothing \to \left(A\preccurlyeq 1_{𝑜}\to A\approx 1_{𝑜}\right)$$
15		iman	$$⊢\left(A\preccurlyeq 1_{𝑜}\to A\approx 1_{𝑜}\right)\leftrightarrow \neg \left(A\preccurlyeq 1_{𝑜}\wedge \neg A\approx 1_{𝑜}\right)$$
16	14 15	sylib	$$⊢A\ne \varnothing \to \neg \left(A\preccurlyeq 1_{𝑜}\wedge \neg A\approx 1_{𝑜}\right)$$
17		brsdom	$$⊢A\prec 1_{𝑜}\leftrightarrow \left(A\preccurlyeq 1_{𝑜}\wedge \neg A\approx 1_{𝑜}\right)$$
18	16 17	sylnibr	$$⊢A\ne \varnothing \to \neg A\prec 1_{𝑜}$$
19	18	necon4ai	$$⊢A\prec 1_{𝑜}\to A=\varnothing$$
20		1n0	$$⊢1_{𝑜}\ne \varnothing$$
21		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
22	21	0sdom	$$⊢\varnothing \prec 1_{𝑜}\leftrightarrow 1_{𝑜}\ne \varnothing$$
23	20 22	mpbir	$$⊢\varnothing \prec 1_{𝑜}$$
24		breq1	$$⊢A=\varnothing \to \left(A\prec 1_{𝑜}\leftrightarrow \varnothing \prec 1_{𝑜}\right)$$
25	23 24	mpbiri	$$⊢A=\varnothing \to A\prec 1_{𝑜}$$
26	19 25	impbii	$$⊢A\prec 1_{𝑜}\leftrightarrow A=\varnothing$$