This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ V → N ∈ UnivVtx ⁡ G ↔ G NeighbVtx N = V ∖ N

Proof

Step Hyp Ref Expression
1 uvtxnbgr.v ⊢ V = Vtx ⁡ G
2 1 uvtxnbgr ⊢ N ∈ UnivVtx ⁡ G → G NeighbVtx N = V ∖ N
3 simpl ⊢ N ∈ V ∧ G NeighbVtx N = V ∖ N → N ∈ V
4 raleleq ⊢ V ∖ N = G NeighbVtx N → ∀ n ∈ V ∖ N n ∈ G NeighbVtx N
5 4 eqcoms ⊢ G NeighbVtx N = V ∖ N → ∀ n ∈ V ∖ N n ∈ G NeighbVtx N
6 5 adantl ⊢ N ∈ V ∧ G NeighbVtx N = V ∖ N → ∀ n ∈ V ∖ N n ∈ G NeighbVtx N
7 1 uvtxel ⊢ N ∈ UnivVtx ⁡ G ↔ N ∈ V ∧ ∀ n ∈ V ∖ N n ∈ G NeighbVtx N
8 3 6 7 sylanbrc ⊢ N ∈ V ∧ G NeighbVtx N = V ∖ N → N ∈ UnivVtx ⁡ G
9 8 ex ⊢ N ∈ V → G NeighbVtx N = V ∖ N → N ∈ UnivVtx ⁡ G
10 2 9 impbid2 ⊢ N ∈ V → N ∈ UnivVtx ⁡ G ↔ G NeighbVtx N = V ∖ N