iscplgr

Description: The property of being a complete graph. (Contributed by AV, 1-Nov-2020)

		Ref	Expression
	Hypothesis	cplgruvtxb.v	$⊢ V = Vtx (G)$
	Assertion	iscplgr	$⊢ G \in W \to (G \in ComplGraph \leftrightarrow \forall v \in V v \in UnivVtx (G))$

Step	Hyp	Ref	Expression
1		cplgruvtxb.v	$⊢ V = Vtx (G)$
2	1	cplgruvtxb	$⊢ G \in W \to (G \in ComplGraph \leftrightarrow UnivVtx (G) = V)$
3		eqss	$⊢ UnivVtx (G) = V \leftrightarrow (UnivVtx (G) \subseteq V \land V \subseteq UnivVtx (G))$
4	1	uvtxssvtx	$⊢ UnivVtx (G) \subseteq V$
5		dfss3	$⊢ V \subseteq UnivVtx (G) \leftrightarrow \forall v \in V v \in UnivVtx (G)$
6	5	anbi2i	$⊢ (UnivVtx (G) \subseteq V \land V \subseteq UnivVtx (G)) \leftrightarrow (UnivVtx (G) \subseteq V \land \forall v \in V v \in UnivVtx (G))$
7	4 6	mpbiran	$⊢ (UnivVtx (G) \subseteq V \land V \subseteq UnivVtx (G)) \leftrightarrow \forall v \in V v \in UnivVtx (G)$
8	3 7	bitri	$⊢ UnivVtx (G) = V \leftrightarrow \forall v \in V v \in UnivVtx (G)$
9	2 8	bitrdi	$⊢ G \in W \to (G \in ComplGraph \leftrightarrow \forall v \in V v \in UnivVtx (G))$

Metamath Proof Explorer