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 e. V | A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) }

Proof

Step Hyp Ref Expression
1 uvtxval.v 
 |-  V = ( Vtx ` G )
2 df-uvtx 
 |-  UnivVtx = ( g e. _V |-> { v e. ( Vtx ` g ) | A. n e. ( ( Vtx ` g ) \ { v } ) n e. ( 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 e. ( g NeighbVtx v ) <-> n e. ( G NeighbVtx v ) ) )
8 5 7 raleqbidv 
 |-  ( g = G -> ( A. n e. ( ( Vtx ` g ) \ { v } ) n e. ( g NeighbVtx v ) <-> A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) )
9 2 8 fvmptrabfv 
 |-  ( UnivVtx ` G ) = { v e. ( Vtx ` G ) | A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) }
10 1 eqcomi 
 |-  ( Vtx ` G ) = V
11 10 rabeqi 
 |-  { v e. ( Vtx ` G ) | A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) } = { v e. V | A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) }
12 9 11 eqtri 
 |-  ( UnivVtx ` G ) = { v e. V | A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) }