Theorem relsnb

Description: An at-most-singleton is a relation iff it is empty (because it is a "singleton on a proper class") or it is a singleton of an ordered pair. (Contributed by BJ, 26-Feb-2023)

	Ref	Expression
Assertion	relsnb	$$⊢\mathrm{Rel}\left\{A\right\}\leftrightarrow \left(\neg A\in \mathrm{V}\vee A\in \left(\mathrm{V}\times \mathrm{V}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		relsng	$$⊢A\in \mathrm{V}\to \left(\mathrm{Rel}\left\{A\right\}\leftrightarrow A\in \left(\mathrm{V}\times \mathrm{V}\right)\right)$$
2	1	biimpcd	$$⊢\mathrm{Rel}\left\{A\right\}\to \left(A\in \mathrm{V}\to A\in \left(\mathrm{V}\times \mathrm{V}\right)\right)$$
3		imor	$$⊢\left(A\in \mathrm{V}\to A\in \left(\mathrm{V}\times \mathrm{V}\right)\right)\leftrightarrow \left(\neg A\in \mathrm{V}\vee A\in \left(\mathrm{V}\times \mathrm{V}\right)\right)$$
4	2 3	sylib	$$⊢\mathrm{Rel}\left\{A\right\}\to \left(\neg A\in \mathrm{V}\vee A\in \left(\mathrm{V}\times \mathrm{V}\right)\right)$$
5		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
6		rel0	$$⊢\mathrm{Rel}\varnothing$$
7		releq	$$⊢\left\{A\right\}=\varnothing \to \left(\mathrm{Rel}\left\{A\right\}\leftrightarrow \mathrm{Rel}\varnothing \right)$$
8	6 7	mpbiri	$$⊢\left\{A\right\}=\varnothing \to \mathrm{Rel}\left\{A\right\}$$
9	5 8	sylbi	$$⊢\neg A\in \mathrm{V}\to \mathrm{Rel}\left\{A\right\}$$
10		relsng	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \left(\mathrm{Rel}\left\{A\right\}\leftrightarrow A\in \left(\mathrm{V}\times \mathrm{V}\right)\right)$$
11	10	ibir	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \mathrm{Rel}\left\{A\right\}$$
12	9 11	jaoi	$$⊢\left(\neg A\in \mathrm{V}\vee A\in \left(\mathrm{V}\times \mathrm{V}\right)\right)\to \mathrm{Rel}\left\{A\right\}$$
13	4 12	impbii	$$⊢\mathrm{Rel}\left\{A\right\}\leftrightarrow \left(\neg A\in \mathrm{V}\vee A\in \left(\mathrm{V}\times \mathrm{V}\right)\right)$$