Metamath Proof Explorer

Theorem cusgr0v

Description: A graph with no vertices and no edges is a complete simple graph. (Contributed by Alexander van der Vekens, 13-Oct-2017) (Revised by AV, 1-Nov-2020)

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

Proof

Step Hyp Ref Expression
1 cplgr0v.v ⊢ V = Vtx ⁡ G
2 1 eqeq1i ⊢ V = ∅ ↔ Vtx ⁡ G = ∅
3 usgr0v ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ iEdg ⁡ G = ∅ → G ∈ USGraph
4 2 3 syl3an2b ⊢ G ∈ W ∧ V = ∅ ∧ iEdg ⁡ G = ∅ → G ∈ USGraph
5 1 cplgr0v ⊢ G ∈ W ∧ V = ∅ → G ∈ ComplGraph
6 5 3adant3 ⊢ G ∈ W ∧ V = ∅ ∧ iEdg ⁡ G = ∅ → G ∈ ComplGraph
7 iscusgr ⊢ G ∈ ComplUSGraph ↔ G ∈ USGraph ∧ G ∈ ComplGraph
8 4 6 7 sylanbrc ⊢ G ∈ W ∧ V = ∅ ∧ iEdg ⁡ G = ∅ → G ∈ ComplUSGraph