Metamath Proof Explorer

Theorem usgr1v0edg

Description: A class with one (or no) vertex is a simple graph if and only if it has no edges. (Contributed by Alexander van der Vekens, 13-Oct-2017) (Revised by AV, 18-Oct-2020)

Ref Expression
Assertion usgr1v0edg ⊢ G ∈ W ∧ Vtx ⁡ G = A ∧ Fun ⁡ iEdg ⁡ G → G ∈ USGraph ↔ Edg ⁡ G = ∅

Proof

Step Hyp Ref Expression
1 usgr1v ⊢ G ∈ W ∧ Vtx ⁡ G = A → G ∈ USGraph ↔ iEdg ⁡ G = ∅
2 1 3adant3 ⊢ G ∈ W ∧ Vtx ⁡ G = A ∧ Fun ⁡ iEdg ⁡ G → G ∈ USGraph ↔ iEdg ⁡ G = ∅
3 funrel ⊢ Fun ⁡ iEdg ⁡ G → Rel ⁡ iEdg ⁡ G
4 relrn0 ⊢ Rel ⁡ iEdg ⁡ G → iEdg ⁡ G = ∅ ↔ ran ⁡ iEdg ⁡ G = ∅
5 3 4 syl ⊢ Fun ⁡ iEdg ⁡ G → iEdg ⁡ G = ∅ ↔ ran ⁡ iEdg ⁡ G = ∅
6 5 3ad2ant3 ⊢ G ∈ W ∧ Vtx ⁡ G = A ∧ Fun ⁡ iEdg ⁡ G → iEdg ⁡ G = ∅ ↔ ran ⁡ iEdg ⁡ G = ∅
7 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
8 7 eqcomi ⊢ ran ⁡ iEdg ⁡ G = Edg ⁡ G
9 8 eqeq1i ⊢ ran ⁡ iEdg ⁡ G = ∅ ↔ Edg ⁡ G = ∅
10 9 a1i ⊢ G ∈ W ∧ Vtx ⁡ G = A ∧ Fun ⁡ iEdg ⁡ G → ran ⁡ iEdg ⁡ G = ∅ ↔ Edg ⁡ G = ∅
11 2 6 10 3bitrd ⊢ G ∈ W ∧ Vtx ⁡ G = A ∧ Fun ⁡ iEdg ⁡ G → G ∈ USGraph ↔ Edg ⁡ G = ∅