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