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 ∖ N k N ∈ 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 ∖ v k v ∈ E
4 3 eleq2d ⊢ G ∈ USGraph → N ∈ UnivVtx ⁡ G ↔ N ∈ v ∈ V | ∀ k ∈ V ∖ v k v ∈ E
5 sneq ⊢ v = N → v = N
6 5 difeq2d ⊢ v = N → V ∖ v = V ∖ N
7 preq2 ⊢ v = N → k v = k N
8 7 eleq1d ⊢ v = N → k v ∈ E ↔ k N ∈ E
9 6 8 raleqbidv ⊢ v = N → ∀ k ∈ V ∖ v k v ∈ E ↔ ∀ k ∈ V ∖ N k N ∈ E
10 9 elrab ⊢ N ∈ v ∈ V | ∀ k ∈ V ∖ v k v ∈ E ↔ N ∈ V ∧ ∀ k ∈ V ∖ N k N ∈ E
11 4 10 bitrdi ⊢ G ∈ USGraph → N ∈ UnivVtx ⁡ G ↔ N ∈ V ∧ ∀ k ∈ V ∖ N k N ∈ E