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=∅