Metamath Proof Explorer

Theorem isuvtx

Description: The set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 30-Oct-2020) (Revised by AV, 14-Feb-2022)

Ref Expression
Hypotheses uvtxel.v ⊢V=Vtx⁡G
isuvtx.e ⊢E=Edg⁡G
Assertion isuvtx ⊢UnivVtx⁡G=v∈V|∀k∈V∖v∃e∈Ekv⊆e

Proof

Step Hyp Ref Expression
1 uvtxel.v ⊢V=Vtx⁡G
2 isuvtx.e ⊢E=Edg⁡G
3 1 uvtxval ⊢UnivVtx⁡G=v∈V|∀k∈V∖vk∈GNeighbVtxv
4 1 2 nbgrel ⊢k∈GNeighbVtxv↔k∈V∧v∈V∧k≠v∧∃e∈Evk⊆e
5 df-3an ⊢k∈V∧v∈V∧k≠v∧∃e∈Evk⊆e↔k∈V∧v∈V∧k≠v∧∃e∈Evk⊆e
6 4 5 bitri ⊢k∈GNeighbVtxv↔k∈V∧v∈V∧k≠v∧∃e∈Evk⊆e
7 prcom ⊢kv=vk
8 7 sseq1i ⊢kv⊆e↔vk⊆e
9 8 rexbii ⊢∃e∈Ekv⊆e↔∃e∈Evk⊆e
10 id ⊢v∈V→v∈V
11 eldifi ⊢k∈V∖v→k∈V
12 10 11 anim12ci ⊢v∈V∧k∈V∖v→k∈V∧v∈V
13 eldifsni ⊢k∈V∖v→k≠v
14 13 adantl ⊢v∈V∧k∈V∖v→k≠v
15 12 14 jca ⊢v∈V∧k∈V∖v→k∈V∧v∈V∧k≠v
16 15 biantrurd ⊢v∈V∧k∈V∖v→∃e∈Evk⊆e↔k∈V∧v∈V∧k≠v∧∃e∈Evk⊆e
17 9 16 bitr2id ⊢v∈V∧k∈V∖v→k∈V∧v∈V∧k≠v∧∃e∈Evk⊆e↔∃e∈Ekv⊆e
18 6 17 bitrid ⊢v∈V∧k∈V∖v→k∈GNeighbVtxv↔∃e∈Ekv⊆e
19 18 ralbidva ⊢v∈V→∀k∈V∖vk∈GNeighbVtxv↔∀k∈V∖v∃e∈Ekv⊆e
20 19 rabbiia ⊢v∈V|∀k∈V∖vk∈GNeighbVtxv=v∈V|∀k∈V∖v∃e∈Ekv⊆e
21 3 20 eqtri ⊢UnivVtx⁡G=v∈V|∀k∈V∖v∃e∈Ekv⊆e