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=∅