Metamath Proof Explorer

Theorem cusgr1v

Description: A graph with one vertex and no edges is a complete simple graph. (Contributed by AV, 1-Nov-2020) (Revised by AV, 23-Mar-2021)

Ref Expression
Hypothesis cplgr0v.v ⊢V=Vtx⁡G
Assertion cusgr1v ⊢V=1∧iEdg⁡G=∅→G∈ComplUSGraph

Proof

Step Hyp Ref Expression
1 cplgr0v.v ⊢V=Vtx⁡G
2 1 cplgr1vlem ⊢V=1→G∈V
3 2 adantr ⊢V=1∧iEdg⁡G=∅→G∈V
4 simpr ⊢V=1∧iEdg⁡G=∅→iEdg⁡G=∅
5 3 4 usgr0e ⊢V=1∧iEdg⁡G=∅→G∈USGraph
6 1 cplgr1v ⊢V=1→G∈ComplGraph
7 6 adantr ⊢V=1∧iEdg⁡G=∅→G∈ComplGraph
8 iscusgr ⊢G∈ComplUSGraph↔G∈USGraph∧G∈ComplGraph
9 5 7 8 sylanbrc ⊢V=1∧iEdg⁡G=∅→G∈ComplUSGraph