cplgr0v

Description: A null graph (with no vertices) is a complete 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	cplgr0v	$⊢ (G \in W \land V = \emptyset) \to G \in ComplGraph$

Proof

Step	Hyp	Ref	Expression
1		cplgr0v.v	$⊢ V = Vtx (G)$
2		rzal	$⊢ V = \emptyset \to \forall v \in V v \in UnivVtx (G)$
3	2	adantl	$⊢ (G \in W \land V = \emptyset) \to \forall v \in V v \in UnivVtx (G)$
4	1	iscplgr	$⊢ G \in W \to (G \in ComplGraph \leftrightarrow \forall v \in V v \in UnivVtx (G))$
5	4	adantr	$⊢ (G \in W \land V = \emptyset) \to (G \in ComplGraph \leftrightarrow \forall v \in V v \in UnivVtx (G))$
6	3 5	mpbird	$⊢ (G \in W \land V = \emptyset) \to G \in ComplGraph$

Metamath Proof Explorer

Theorem cplgr0v

Proof