Theorem mo0sn

Description: Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Assertion	mo0sn	$$⊢{\exists }^{*}xx\in A\leftrightarrow \left(A=\varnothing \vee \exists yA=\left\{y\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢Ⅎzx\in A$$
2		nfv	$$⊢Ⅎxz\in A$$
3		eleq1w	$$⊢x=z\to \left(x\in A\leftrightarrow z\in A\right)$$
4	1 2 3	cbvmow	$$⊢{\exists }^{*}xx\in A\leftrightarrow {\exists }^{*}zz\in A$$
5		neq0	$$⊢\neg A=\varnothing \leftrightarrow \exists zz\in A$$
6	5	anbi1i	$$⊢\left(\neg A=\varnothing \wedge {\exists }^{*}zz\in A\right)\leftrightarrow \left(\exists zz\in A\wedge {\exists }^{*}zz\in A\right)$$
7		df-eu	$$⊢\exists !zz\in A\leftrightarrow \left(\exists zz\in A\wedge {\exists }^{*}zz\in A\right)$$
8		eu6	$$⊢\exists !zz\in A\leftrightarrow \exists y\forall z\left(z\in A\leftrightarrow z=y\right)$$
9	6 7 8	3bitr2i	$$⊢\left(\neg A=\varnothing \wedge {\exists }^{*}zz\in A\right)\leftrightarrow \exists y\forall z\left(z\in A\leftrightarrow z=y\right)$$
10		dfcleq	$$⊢A=\left\{y\right\}\leftrightarrow \forall z\left(z\in A\leftrightarrow z\in \left\{y\right\}\right)$$
11		velsn	$$⊢z\in \left\{y\right\}\leftrightarrow z=y$$
12	11	bibi2i	$$⊢\left(z\in A\leftrightarrow z\in \left\{y\right\}\right)\leftrightarrow \left(z\in A\leftrightarrow z=y\right)$$
13	12	albii	$$⊢\forall z\left(z\in A\leftrightarrow z\in \left\{y\right\}\right)\leftrightarrow \forall z\left(z\in A\leftrightarrow z=y\right)$$
14	10 13	sylbbr	$$⊢\forall z\left(z\in A\leftrightarrow z=y\right)\to A=\left\{y\right\}$$
15	14	eximi	$$⊢\exists y\forall z\left(z\in A\leftrightarrow z=y\right)\to \exists yA=\left\{y\right\}$$
16	9 15	sylbi	$$⊢\left(\neg A=\varnothing \wedge {\exists }^{*}zz\in A\right)\to \exists yA=\left\{y\right\}$$
17	16	expcom	$$⊢{\exists }^{*}zz\in A\to \left(\neg A=\varnothing \to \exists yA=\left\{y\right\}\right)$$
18	17	orrd	$$⊢{\exists }^{*}zz\in A\to \left(A=\varnothing \vee \exists yA=\left\{y\right\}\right)$$
19		mo0	$$⊢A=\varnothing \to {\exists }^{*}zz\in A$$
20		mosn	$$⊢A=\left\{y\right\}\to {\exists }^{*}zz\in A$$
21	20	exlimiv	$$⊢\exists yA=\left\{y\right\}\to {\exists }^{*}zz\in A$$
22	19 21	jaoi	$$⊢\left(A=\varnothing \vee \exists yA=\left\{y\right\}\right)\to {\exists }^{*}zz\in A$$
23	18 22	impbii	$$⊢{\exists }^{*}zz\in A\leftrightarrow \left(A=\varnothing \vee \exists yA=\left\{y\right\}\right)$$
24	4 23	bitri	$$⊢{\exists }^{*}xx\in A\leftrightarrow \left(A=\varnothing \vee \exists yA=\left\{y\right\}\right)$$