Metamath Proof Explorer

Theorem nbcplgr

Description: In a complete graph, each vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 3-Nov-2020)

		Ref	Expression
	Hypothesis	nbcplgr.v	$⊢ V = Vtx (G)$
	Assertion	nbcplgr	$⊢ (G \in ComplGraph \land N \in V) \to G NeighbVtx N = V ∖ \{N\}$

Proof

Step	Hyp	Ref	Expression
1		nbcplgr.v	$⊢ V = Vtx (G)$
2	1	cplgruvtxb	$⊢ G \in ComplGraph \to (G \in ComplGraph \leftrightarrow UnivVtx (G) = V)$
3	2	ibi	$⊢ G \in ComplGraph \to UnivVtx (G) = V$
4	3	eqcomd	$⊢ G \in ComplGraph \to V = UnivVtx (G)$
5	4	eleq2d	$⊢ G \in ComplGraph \to (N \in V \leftrightarrow N \in UnivVtx (G))$
6	5	biimpa	$⊢ (G \in ComplGraph \land N \in V) \to N \in UnivVtx (G)$
7	1	uvtxnbgrb	$⊢ N \in V \to (N \in UnivVtx (G) \leftrightarrow G NeighbVtx N = V ∖ \{N\})$
8	7	adantl	$⊢ (G \in ComplGraph \land N \in V) \to (N \in UnivVtx (G) \leftrightarrow G NeighbVtx N = V ∖ \{N\})$
9	6 8	mpbid	$⊢ (G \in ComplGraph \land N \in V) \to G NeighbVtx N = V ∖ \{N\}$