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 𝑣 ∈ ∅ 𝑣 ∈ ( UnivVtx ‘ ∅ )
2 vtxval0 ( Vtx ‘ ∅ ) = ∅
3 2 raleqi ( ∀ 𝑣 ∈ ( Vtx ‘ ∅ ) 𝑣 ∈ ( UnivVtx ‘ ∅ ) ↔ ∀ 𝑣 ∈ ∅ 𝑣 ∈ ( UnivVtx ‘ ∅ ) )
4 1 3 mpbir 𝑣 ∈ ( Vtx ‘ ∅ ) 𝑣 ∈ ( UnivVtx ‘ ∅ )
5 0ex ∅ ∈ V
6 eqid ( Vtx ‘ ∅ ) = ( Vtx ‘ ∅ )
7 6 iscplgr ( ∅ ∈ V → ( ∅ ∈ ComplGraph ↔ ∀ 𝑣 ∈ ( Vtx ‘ ∅ ) 𝑣 ∈ ( UnivVtx ‘ ∅ ) ) )
8 5 7 ax-mp ( ∅ ∈ ComplGraph ↔ ∀ 𝑣 ∈ ( Vtx ‘ ∅ ) 𝑣 ∈ ( UnivVtx ‘ ∅ ) )
9 4 8 mpbir ∅ ∈ ComplGraph