Metamath Proof Explorer

Theorem usgr0vb

Description: The null graph, with no vertices, is a simple graph iff the edge function is empty. (Contributed by Alexander van der Vekens, 30-Sep-2017) (Revised by AV, 16-Oct-2020)

Ref Expression
Assertion usgr0vb ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → G ∈ USGraph ↔ iEdg ⁡ G = ∅

Proof

Step Hyp Ref Expression
1 usgruhgr ⊢ G ∈ USGraph → G ∈ UHGraph
2 uhgr0vb ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → G ∈ UHGraph ↔ iEdg ⁡ G = ∅
3 1 2 syl5ib ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → G ∈ USGraph → iEdg ⁡ G = ∅
4 simpl ⊢ G ∈ W ∧ iEdg ⁡ G = ∅ → G ∈ W
5 simpr ⊢ G ∈ W ∧ iEdg ⁡ G = ∅ → iEdg ⁡ G = ∅
6 4 5 usgr0e ⊢ G ∈ W ∧ iEdg ⁡ G = ∅ → G ∈ USGraph
7 6 ex ⊢ G ∈ W → iEdg ⁡ G = ∅ → G ∈ USGraph
8 7 adantr ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → iEdg ⁡ G = ∅ → G ∈ USGraph
9 3 8 impbid ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → G ∈ USGraph ↔ iEdg ⁡ G = ∅