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 { 𝐴 } ↔ ( ¬ 𝐴 ∈ V ∨ 𝐴 ∈ ( V × V ) ) )

Proof

Step	Hyp	Ref	Expression
1		relsng	⊢ ( 𝐴 ∈ V → ( Rel { 𝐴 } ↔ 𝐴 ∈ ( V × V ) ) )
2	1	biimpcd	⊢ ( Rel { 𝐴 } → ( 𝐴 ∈ V → 𝐴 ∈ ( V × V ) ) )
3		imor	⊢ ( ( 𝐴 ∈ V → 𝐴 ∈ ( V × V ) ) ↔ ( ¬ 𝐴 ∈ V ∨ 𝐴 ∈ ( V × V ) ) )
4	2 3	sylib	⊢ ( Rel { 𝐴 } → ( ¬ 𝐴 ∈ V ∨ 𝐴 ∈ ( V × V ) ) )
5		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
6		rel0	⊢ Rel ∅
7		releq	⊢ ( { 𝐴 } = ∅ → ( Rel { 𝐴 } ↔ Rel ∅ ) )
8	6 7	mpbiri	⊢ ( { 𝐴 } = ∅ → Rel { 𝐴 } )
9	5 8	sylbi	⊢ ( ¬ 𝐴 ∈ V → Rel { 𝐴 } )
10		relsng	⊢ ( 𝐴 ∈ ( V × V ) → ( Rel { 𝐴 } ↔ 𝐴 ∈ ( V × V ) ) )
11	10	ibir	⊢ ( 𝐴 ∈ ( V × V ) → Rel { 𝐴 } )
12	9 11	jaoi	⊢ ( ( ¬ 𝐴 ∈ V ∨ 𝐴 ∈ ( V × V ) ) → Rel { 𝐴 } )
13	4 12	impbii	⊢ ( Rel { 𝐴 } ↔ ( ¬ 𝐴 ∈ V ∨ 𝐴 ∈ ( V × V ) ) )