Metamath Proof Explorer

Theorem uvtxval

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

Ref Expression
Hypothesis uvtxval.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
Assertion uvtxval ${⊢}\mathrm{UnivVtx}\left({G}\right)=\left\{{v}\in {V}|\forall {n}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\in \left({G}\mathrm{NeighbVtx}{v}\right)\right\}$

Proof

Step Hyp Ref Expression
1 uvtxval.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 df-uvtx ${⊢}\mathrm{UnivVtx}=\left({g}\in \mathrm{V}⟼\left\{{v}\in \mathrm{Vtx}\left({g}\right)|\forall {n}\in \left(\mathrm{Vtx}\left({g}\right)\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\in \left({g}\mathrm{NeighbVtx}{v}\right)\right\}\right)$
3 fveq2 ${⊢}{g}={G}\to \mathrm{Vtx}\left({g}\right)=\mathrm{Vtx}\left({G}\right)$
4 3 1 eqtr4di ${⊢}{g}={G}\to \mathrm{Vtx}\left({g}\right)={V}$
5 4 difeq1d ${⊢}{g}={G}\to \mathrm{Vtx}\left({g}\right)\setminus \left\{{v}\right\}={V}\setminus \left\{{v}\right\}$
6 oveq1 ${⊢}{g}={G}\to {g}\mathrm{NeighbVtx}{v}={G}\mathrm{NeighbVtx}{v}$
7 6 eleq2d ${⊢}{g}={G}\to \left({n}\in \left({g}\mathrm{NeighbVtx}{v}\right)↔{n}\in \left({G}\mathrm{NeighbVtx}{v}\right)\right)$
8 5 7 raleqbidv ${⊢}{g}={G}\to \left(\forall {n}\in \left(\mathrm{Vtx}\left({g}\right)\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\in \left({g}\mathrm{NeighbVtx}{v}\right)↔\forall {n}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\in \left({G}\mathrm{NeighbVtx}{v}\right)\right)$
9 2 8 fvmptrabfv ${⊢}\mathrm{UnivVtx}\left({G}\right)=\left\{{v}\in \mathrm{Vtx}\left({G}\right)|\forall {n}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\in \left({G}\mathrm{NeighbVtx}{v}\right)\right\}$
10 1 eqcomi ${⊢}\mathrm{Vtx}\left({G}\right)={V}$
11 10 rabeqi ${⊢}\left\{{v}\in \mathrm{Vtx}\left({G}\right)|\forall {n}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\in \left({G}\mathrm{NeighbVtx}{v}\right)\right\}=\left\{{v}\in {V}|\forall {n}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\in \left({G}\mathrm{NeighbVtx}{v}\right)\right\}$
12 9 11 eqtri ${⊢}\mathrm{UnivVtx}\left({G}\right)=\left\{{v}\in {V}|\forall {n}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\in \left({G}\mathrm{NeighbVtx}{v}\right)\right\}$