Metamath Proof Explorer

Theorem usgr1vr

Description: A simple graph with one vertex has no edges. (Contributed by AV, 18-Oct-2020) (Revised by AV, 21-Mar-2021) (Proof shortened by AV, 2-Apr-2021)

Ref Expression
Assertion usgr1vr ⊢ A ∈ X ∧ Vtx ⁡ G = A → G ∈ USGraph → iEdg ⁡ G = ∅

Proof

Step Hyp Ref Expression
1 usgruhgr ⊢ G ∈ USGraph → G ∈ UHGraph
2 1 adantl ⊢ A ∈ X ∧ Vtx ⁡ G = A ∧ G ∈ USGraph → G ∈ UHGraph
3 fveq2 ⊢ Vtx ⁡ G = A → Vtx ⁡ G = A
4 hashsng ⊢ A ∈ X → A = 1
5 3 4 sylan9eqr ⊢ A ∈ X ∧ Vtx ⁡ G = A → Vtx ⁡ G = 1
6 5 adantr ⊢ A ∈ X ∧ Vtx ⁡ G = A ∧ G ∈ USGraph → Vtx ⁡ G = 1
7 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
8 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
9 7 8 usgrislfuspgr ⊢ G ∈ USGraph ↔ G ∈ USHGraph ∧ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G | 2 ≤ x
10 9 simprbi ⊢ G ∈ USGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G | 2 ≤ x
11 10 adantl ⊢ A ∈ X ∧ Vtx ⁡ G = A ∧ G ∈ USGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G | 2 ≤ x
12 eqid ⊢ x ∈ 𝒫 Vtx ⁡ G | 2 ≤ x = x ∈ 𝒫 Vtx ⁡ G | 2 ≤ x
13 7 8 12 lfuhgr1v0e ⊢ G ∈ UHGraph ∧ Vtx ⁡ G = 1 ∧ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G | 2 ≤ x → Edg ⁡ G = ∅
14 2 6 11 13 syl3anc ⊢ A ∈ X ∧ Vtx ⁡ G = A ∧ G ∈ USGraph → Edg ⁡ G = ∅
15 uhgriedg0edg0 ⊢ G ∈ UHGraph → Edg ⁡ G = ∅ ↔ iEdg ⁡ G = ∅
16 1 15 syl ⊢ G ∈ USGraph → Edg ⁡ G = ∅ ↔ iEdg ⁡ G = ∅
17 16 adantl ⊢ A ∈ X ∧ Vtx ⁡ G = A ∧ G ∈ USGraph → Edg ⁡ G = ∅ ↔ iEdg ⁡ G = ∅
18 14 17 mpbid ⊢ A ∈ X ∧ Vtx ⁡ G = A ∧ G ∈ USGraph → iEdg ⁡ G = ∅
19 18 ex ⊢ A ∈ X ∧ Vtx ⁡ G = A → G ∈ USGraph → iEdg ⁡ G = ∅