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	|- ( Rel { A } <-> ( -. A e. _V \/ A e. ( _V X. _V ) ) )

Proof

Step	Hyp	Ref	Expression
1		relsng	|- ( A e. _V -> ( Rel { A } <-> A e. ( _V X. _V ) ) )
2	1	biimpcd	|- ( Rel { A } -> ( A e. _V -> A e. ( _V X. _V ) ) )
3		imor	|- ( ( A e. _V -> A e. ( _V X. _V ) ) <-> ( -. A e. _V \/ A e. ( _V X. _V ) ) )
4	2 3	sylib	|- ( Rel { A } -> ( -. A e. _V \/ A e. ( _V X. _V ) ) )
5		snprc	|- ( -. A e. _V <-> { A } = (/) )
6		rel0	|- Rel (/)
7		releq	|- ( { A } = (/) -> ( Rel { A } <-> Rel (/) ) )
8	6 7	mpbiri	|- ( { A } = (/) -> Rel { A } )
9	5 8	sylbi	|- ( -. A e. _V -> Rel { A } )
10		relsng	|- ( A e. ( _V X. _V ) -> ( Rel { A } <-> A e. ( _V X. _V ) ) )
11	10	ibir	|- ( A e. ( _V X. _V ) -> Rel { A } )
12	9 11	jaoi	|- ( ( -. A e. _V \/ A e. ( _V X. _V ) ) -> Rel { A } )
13	4 12	impbii	|- ( Rel { A } <-> ( -. A e. _V \/ A e. ( _V X. _V ) ) )