Metamath Proof Explorer

Theorem uhgr0v0e

Description: The null graph, with no vertices, has no edges. (Contributed by AV, 21-Oct-2020)

Ref Expression
Hypotheses uhgr0v0e.v ⊢ V = Vtx ⁡ G
uhgr0v0e.e ⊢ E = Edg ⁡ G
Assertion uhgr0v0e ⊢ G ∈ UHGraph ∧ V = ∅ → E = ∅

Proof

Step Hyp Ref Expression
1 uhgr0v0e.v ⊢ V = Vtx ⁡ G
2 uhgr0v0e.e ⊢ E = Edg ⁡ G
3 1 eqeq1i ⊢ V = ∅ ↔ Vtx ⁡ G = ∅
4 uhgr0vb ⊢ G ∈ UHGraph ∧ Vtx ⁡ G = ∅ → G ∈ UHGraph ↔ iEdg ⁡ G = ∅
5 4 biimpd ⊢ G ∈ UHGraph ∧ Vtx ⁡ G = ∅ → G ∈ UHGraph → iEdg ⁡ G = ∅
6 5 ex ⊢ G ∈ UHGraph → Vtx ⁡ G = ∅ → G ∈ UHGraph → iEdg ⁡ G = ∅
7 3 6 biimtrid ⊢ G ∈ UHGraph → V = ∅ → G ∈ UHGraph → iEdg ⁡ G = ∅
8 7 pm2.43a ⊢ G ∈ UHGraph → V = ∅ → iEdg ⁡ G = ∅
9 8 imp ⊢ G ∈ UHGraph ∧ V = ∅ → iEdg ⁡ G = ∅
10 2 eqeq1i ⊢ E = ∅ ↔ Edg ⁡ G = ∅
11 uhgriedg0edg0 ⊢ G ∈ UHGraph → Edg ⁡ G = ∅ ↔ iEdg ⁡ G = ∅
12 10 11 bitrid ⊢ G ∈ UHGraph → E = ∅ ↔ iEdg ⁡ G = ∅
13 12 adantr ⊢ G ∈ UHGraph ∧ V = ∅ → E = ∅ ↔ iEdg ⁡ G = ∅
14 9 13 mpbird ⊢ G ∈ UHGraph ∧ V = ∅ → E = ∅