This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Undirected graphs Neighbors, complete graphs and universal vertices Universal vertices uvtxel
Description: A universal vertex, i.e. an element of the set of all universal
vertices. (Contributed by Alexander van der Vekens , 12-Oct-2017)
(Revised by AV , 29-Oct-2020) (Revised by AV , 14-Feb-2022)
Ref
Expression
Hypothesis
uvtxel.v ⊢ V = Vtx G
Assertion
uvtxel ⊢ N ∈ UnivVtx G ↔ N ∈ V ∧ ∀ n ∈ V ∖ N n ∈ G NeighbVtx N
Proof
Step
Hyp
Ref
Expression
1
uvtxel.v ⊢ V = Vtx G
2
sneq ⊢ v = N → v = N
3
2
difeq2d ⊢ v = N → V ∖ v = V ∖ N
4
oveq2 ⊢ v = N → G NeighbVtx v = G NeighbVtx N
5
4
eleq2d ⊢ v = N → n ∈ G NeighbVtx v ↔ n ∈ G NeighbVtx N
6
3 5
raleqbidv ⊢ v = N → ∀ n ∈ V ∖ v n ∈ G NeighbVtx v ↔ ∀ n ∈ V ∖ N n ∈ G NeighbVtx N
7
1
uvtxval ⊢ UnivVtx G = v ∈ V | ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
8
6 7
elrab2 ⊢ N ∈ UnivVtx G ↔ N ∈ V ∧ ∀ n ∈ V ∖ N n ∈ G NeighbVtx N