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 biimtrdi ⊢ 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