Metamath Proof Explorer

Theorem cplgr0

Description: The null graph (with no vertices and no edges) represented by the empty set is a complete graph. (Contributed by AV, 1-Nov-2020)

Ref Expression
Assertion cplgr0 ⊢∅∈ComplGraph

Proof

Step Hyp Ref Expression
1 ral0 ⊢∀v∈∅v∈UnivVtx⁡∅
2 vtxval0 ⊢Vtx⁡∅=∅
3 2 raleqi ⊢∀v∈Vtx⁡∅v∈UnivVtx⁡∅↔∀v∈∅v∈UnivVtx⁡∅
4 1 3 mpbir ⊢∀v∈Vtx⁡∅v∈UnivVtx⁡∅
5 0ex ⊢∅∈V
6 eqid ⊢Vtx⁡∅=Vtx⁡∅
7 6 iscplgr ⊢∅∈V→∅∈ComplGraph↔∀v∈Vtx⁡∅v∈UnivVtx⁡∅
8 5 7 ax-mp ⊢∅∈ComplGraph↔∀v∈Vtx⁡∅v∈UnivVtx⁡∅
9 4 8 mpbir ⊢∅∈ComplGraph