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