Metamath Proof Explorer

Theorem edg0usgr

Description: A class without edges is a simple graph. Since ran F = (/) does not generally imply Fun F , but Fun ( iEdgG ) is required for G to be a simple graph, however, this must be provided as assertion. (Contributed by AV, 18-Oct-2020)

Ref Expression
Assertion edg0usgr ⊢G∈W∧Edg⁡G=∅∧Fun⁡iEdg⁡G→G∈USGraph

Proof

Step Hyp Ref Expression
1 edgval ⊢Edg⁡G=ran⁡iEdg⁡G
2 1 a1i ⊢G∈W→Edg⁡G=ran⁡iEdg⁡G
3 2 eqeq1d ⊢G∈W→Edg⁡G=∅↔ran⁡iEdg⁡G=∅
4 funrel ⊢Fun⁡iEdg⁡G→Rel⁡iEdg⁡G
5 relrn0 ⊢Rel⁡iEdg⁡G→iEdg⁡G=∅↔ran⁡iEdg⁡G=∅
6 5 bicomd ⊢Rel⁡iEdg⁡G→ran⁡iEdg⁡G=∅↔iEdg⁡G=∅
7 4 6 syl ⊢Fun⁡iEdg⁡G→ran⁡iEdg⁡G=∅↔iEdg⁡G=∅
8 simpr ⊢iEdg⁡G=∅∧G∈W→G∈W
9 simpl ⊢iEdg⁡G=∅∧G∈W→iEdg⁡G=∅
10 8 9 usgr0e ⊢iEdg⁡G=∅∧G∈W→G∈USGraph
11 10 ex ⊢iEdg⁡G=∅→G∈W→G∈USGraph
12 7 11 syl6bi ⊢Fun⁡iEdg⁡G→ran⁡iEdg⁡G=∅→G∈W→G∈USGraph
13 12 com13 ⊢G∈W→ran⁡iEdg⁡G=∅→Fun⁡iEdg⁡G→G∈USGraph
14 3 13 sylbid ⊢G∈W→Edg⁡G=∅→Fun⁡iEdg⁡G→G∈USGraph
15 14 3imp ⊢G∈W∧Edg⁡G=∅∧Fun⁡iEdg⁡G→G∈USGraph