Theorem sdom1

Description: A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		domnsym	$$⊢1_{𝑜}\preccurlyeq A\to \neg A\prec 1_{𝑜}$$
2	1	con2i	$$⊢A\prec 1_{𝑜}\to \neg 1_{𝑜}\preccurlyeq A$$
3		0sdom1dom	$$⊢\varnothing \prec A\leftrightarrow 1_{𝑜}\preccurlyeq A$$
4	2 3	sylnibr	$$⊢A\prec 1_{𝑜}\to \neg \varnothing \prec A$$
5		relsdom	$$⊢\mathrm{Rel}\prec$$
6	5	brrelex1i	$$⊢A\prec 1_{𝑜}\to A\in \mathrm{V}$$
7		0sdomg	$$⊢A\in \mathrm{V}\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
8	7	necon2bbid	$$⊢A\in \mathrm{V}\to \left(A=\varnothing \leftrightarrow \neg \varnothing \prec A\right)$$
9	6 8	syl	$$⊢A\prec 1_{𝑜}\to \left(A=\varnothing \leftrightarrow \neg \varnothing \prec A\right)$$
10	4 9	mpbird	$$⊢A\prec 1_{𝑜}\to A=\varnothing$$
11		1n0	$$⊢1_{𝑜}\ne \varnothing$$
12		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
13	12	0sdom	$$⊢\varnothing \prec 1_{𝑜}\leftrightarrow 1_{𝑜}\ne \varnothing$$
14	11 13	mpbir	$$⊢\varnothing \prec 1_{𝑜}$$
15		breq1	$$⊢A=\varnothing \to \left(A\prec 1_{𝑜}\leftrightarrow \varnothing \prec 1_{𝑜}\right)$$
16	14 15	mpbiri	$$⊢A=\varnothing \to A\prec 1_{𝑜}$$
17	10 16	impbii	$$⊢A\prec 1_{𝑜}\leftrightarrow A=\varnothing$$