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 ∈ V ∨ A ∈ V × V

Proof

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