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