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