Metamath Proof Explorer

Theorem uvtxusgrel

Description: A universal vertex, i.e. an element of the set of all universal vertices, of a simple graph. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 31-Oct-2020)

Ref Expression
Hypotheses uvtxnbgr.v ⊢V=Vtx⁡G
uvtxusgr.e ⊢E=Edg⁡G
Assertion uvtxusgrel ⊢G∈USGraph→N∈UnivVtx⁡G↔N∈V∧∀k∈V∖NkN∈E

Proof

Step Hyp Ref Expression
1 uvtxnbgr.v ⊢V=Vtx⁡G
2 uvtxusgr.e ⊢E=Edg⁡G
3 1 2 uvtxusgr ⊢G∈USGraph→UnivVtx⁡G=v∈V|∀k∈V∖vkv∈E
4 3 eleq2d ⊢G∈USGraph→N∈UnivVtx⁡G↔N∈v∈V|∀k∈V∖vkv∈E
5 sneq ⊢v=N→v=N
6 5 difeq2d ⊢v=N→V∖v=V∖N
7 preq2 ⊢v=N→kv=kN
8 7 eleq1d ⊢v=N→kv∈E↔kN∈E
9 6 8 raleqbidv ⊢v=N→∀k∈V∖vkv∈E↔∀k∈V∖NkN∈E
10 9 elrab ⊢N∈v∈V|∀k∈V∖vkv∈E↔N∈V∧∀k∈V∖NkN∈E
11 4 10 bitrdi ⊢G∈USGraph→N∈UnivVtx⁡G↔N∈V∧∀k∈V∖NkN∈E