Metamath Proof Explorer

Theorem uvtxnbgrb

Description: A vertex is universal iff all the other vertices are its neighbors. (Contributed by Alexander van der Vekens, 13-Jul-2018) (Revised by AV, 3-Nov-2020) (Revised by AV, 23-Mar-2021) (Proof shortened by AV, 14-Feb-2022)

		Ref	Expression
	Hypothesis	uvtxnbgr.v	$⊢ V = Vtx (G)$
	Assertion	uvtxnbgrb	$⊢ N \in V \to (N \in UnivVtx (G) \leftrightarrow G NeighbVtx N = V ∖ \{N\})$

Proof

Step	Hyp	Ref	Expression
1		uvtxnbgr.v	$⊢ V = Vtx (G)$
2	1	uvtxnbgr	$⊢ N \in UnivVtx (G) \to G NeighbVtx N = V ∖ \{N\}$
3		simpl	$⊢ (N \in V \land G NeighbVtx N = V ∖ \{N\}) \to N \in V$
4		raleleq	$⊢ V ∖ \{N\} = G NeighbVtx N \to \forall n \in (V ∖ \{N\}) n \in (G NeighbVtx N)$
5	4	eqcoms	$⊢ G NeighbVtx N = V ∖ \{N\} \to \forall n \in (V ∖ \{N\}) n \in (G NeighbVtx N)$
6	5	adantl	$⊢ (N \in V \land G NeighbVtx N = V ∖ \{N\}) \to \forall n \in (V ∖ \{N\}) n \in (G NeighbVtx N)$
7	1	uvtxel	$⊢ N \in UnivVtx (G) \leftrightarrow (N \in V \land \forall n \in (V ∖ \{N\}) n \in (G NeighbVtx N))$
8	3 6 7	sylanbrc	$⊢ (N \in V \land G NeighbVtx N = V ∖ \{N\}) \to N \in UnivVtx (G)$
9	8	ex	$⊢ N \in V \to (G NeighbVtx N = V ∖ \{N\} \to N \in UnivVtx (G))$
10	2 9	impbid2	$⊢ N \in V \to (N \in UnivVtx (G) \leftrightarrow G NeighbVtx N = V ∖ \{N\})$