This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion uvtxval ( UnivVtx ‘ 𝐺 ) = { 𝑣 ∈ 𝑉 ∣ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) }

Proof

Step Hyp Ref Expression
1 uvtxval.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 df-uvtx ⊢ UnivVtx = ( 𝑔 ∈ V ↦ { 𝑣 ∈ ( Vtx ‘ 𝑔 ) ∣ ∀ 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) 𝑛 ∈ ( 𝑔 NeighbVtx 𝑣 ) } )
3 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
4 3 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 )
5 4 difeq1d ⊢ ( 𝑔 = 𝐺 → ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) = ( 𝑉 ∖ { 𝑣 } ) )
6 oveq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 NeighbVtx 𝑣 ) = ( 𝐺 NeighbVtx 𝑣 ) )
7 6 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑛 ∈ ( 𝑔 NeighbVtx 𝑣 ) ↔ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
8 5 7 raleqbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) 𝑛 ∈ ( 𝑔 NeighbVtx 𝑣 ) ↔ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
9 2 8 fvmptrabfv ⊢ ( UnivVtx ‘ 𝐺 ) = { 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∣ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) }
10 1 eqcomi ⊢ ( Vtx ‘ 𝐺 ) = 𝑉
11 10 rabeqi ⊢ { 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∣ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) } = { 𝑣 ∈ 𝑉 ∣ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) }
12 9 11 eqtri ⊢ ( UnivVtx ‘ 𝐺 ) = { 𝑣 ∈ 𝑉 ∣ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) }