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 = Vtx ⁡ G
Assertion uvtxval ⊢ UnivVtx ⁡ G = v ∈ V | ∀ n ∈ V ∖ v n ∈ G NeighbVtx v

Proof

Step Hyp Ref Expression
1 uvtxval.v ⊢ V = Vtx ⁡ G
2 df-uvtx ⊢ UnivVtx = g ∈ V ⟼ v ∈ Vtx ⁡ g | ∀ n ∈ Vtx ⁡ g ∖ v n ∈ g NeighbVtx v
3 fveq2 ⊢ g = G → Vtx ⁡ g = Vtx ⁡ G
4 3 1 eqtr4di ⊢ g = G → Vtx ⁡ g = V
5 4 difeq1d ⊢ g = G → Vtx ⁡ g ∖ v = V ∖ v
6 oveq1 ⊢ g = G → g NeighbVtx v = G NeighbVtx v
7 6 eleq2d ⊢ g = G → n ∈ g NeighbVtx v ↔ n ∈ G NeighbVtx v
8 5 7 raleqbidv ⊢ g = G → ∀ n ∈ Vtx ⁡ g ∖ v n ∈ g NeighbVtx v ↔ ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
9 2 8 fvmptrabfv ⊢ UnivVtx ⁡ G = v ∈ Vtx ⁡ G | ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
10 1 eqcomi ⊢ Vtx ⁡ G = V
11 10 rabeqi ⊢ v ∈ Vtx ⁡ G | ∀ n ∈ V ∖ v n ∈ G NeighbVtx v = v ∈ V | ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
12 9 11 eqtri ⊢ UnivVtx ⁡ G = v ∈ V | ∀ n ∈ V ∖ v n ∈ G NeighbVtx v