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 uvtx2vtx1edg
Description: If a graph has two vertices, and there is an edge between the vertices,
then each vertex is universal. (Contributed by AV , 1-Nov-2020)
(Revised by AV , 25-Mar-2021) (Proof shortened by AV , 14-Feb-2022)
Ref
Expression
Hypotheses
uvtxel.v ⊢ V = Vtx G
isuvtx.e ⊢ E = Edg G
Assertion
uvtx2vtx1edg ⊢ V = 2 ∧ V ∈ E → ∀ v ∈ V v ∈ UnivVtx G
Proof
Step
Hyp
Ref
Expression
1
uvtxel.v ⊢ V = Vtx G
2
isuvtx.e ⊢ E = Edg G
3
1 2
nbgr2vtx1edg ⊢ V = 2 ∧ V ∈ E → ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
4
1
uvtxel ⊢ v ∈ UnivVtx G ↔ v ∈ V ∧ ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
5
4
a1i ⊢ V = 2 ∧ V ∈ E → v ∈ UnivVtx G ↔ v ∈ V ∧ ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
6
5
baibd ⊢ V = 2 ∧ V ∈ E ∧ v ∈ V → v ∈ UnivVtx G ↔ ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
7
6
ralbidva ⊢ V = 2 ∧ V ∈ E → ∀ v ∈ V v ∈ UnivVtx G ↔ ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
8
3 7
mpbird ⊢ V = 2 ∧ V ∈ E → ∀ v ∈ V v ∈ UnivVtx G