Metamath Proof Explorer

Theorem uvtxusgr

Description: 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 uvtxusgr ⊢ G ∈ USGraph → UnivVtx ⁡ G = n ∈ V | ∀ k ∈ V ∖ n k n ∈ E

Proof

Step Hyp Ref Expression
1 uvtxnbgr.v ⊢ V = Vtx ⁡ G
2 uvtxusgr.e ⊢ E = Edg ⁡ G
3 1 uvtxval ⊢ UnivVtx ⁡ G = n ∈ V | ∀ k ∈ V ∖ n k ∈ G NeighbVtx n
4 2 nbusgreledg ⊢ G ∈ USGraph → k ∈ G NeighbVtx n ↔ k n ∈ E
5 4 ralbidv ⊢ G ∈ USGraph → ∀ k ∈ V ∖ n k ∈ G NeighbVtx n ↔ ∀ k ∈ V ∖ n k n ∈ E
6 5 rabbidv ⊢ G ∈ USGraph → n ∈ V | ∀ k ∈ V ∖ n k ∈ G NeighbVtx n = n ∈ V | ∀ k ∈ V ∖ n k n ∈ E
7 3 6 syl5eq ⊢ G ∈ USGraph → UnivVtx ⁡ G = n ∈ V | ∀ k ∈ V ∖ n k n ∈ E