This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )