Metamath Proof Explorer

Theorem uhgr0vusgr

Description: The null graph, with no vertices, represented by a hypergraph, is a simple graph. (Contributed by AV, 5-Dec-2020)

Ref Expression
Assertion uhgr0vusgr ⊢ G ∈ UHGraph ∧ Vtx ⁡ G = ∅ → G ∈ USGraph

Proof

Step Hyp Ref Expression
1 simpl ⊢ G ∈ UHGraph ∧ Vtx ⁡ G = ∅ → G ∈ UHGraph
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 eqid ⊢ Edg ⁡ G = Edg ⁡ G
4 2 3 uhgr0v0e ⊢ G ∈ UHGraph ∧ Vtx ⁡ G = ∅ → Edg ⁡ G = ∅
5 uhgriedg0edg0 ⊢ G ∈ UHGraph → Edg ⁡ G = ∅ ↔ iEdg ⁡ G = ∅
6 5 adantr ⊢ G ∈ UHGraph ∧ Vtx ⁡ G = ∅ → Edg ⁡ G = ∅ ↔ iEdg ⁡ G = ∅
7 4 6 mpbid ⊢ G ∈ UHGraph ∧ Vtx ⁡ G = ∅ → iEdg ⁡ G = ∅
8 1 7 usgr0e ⊢ G ∈ UHGraph ∧ Vtx ⁡ G = ∅ → G ∈ USGraph