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

Metamath Proof Explorer

Theorem uvtxusgrel

Description: A universal vertex, i.e. an element of the set of all universal vertices, of a simple graph. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 31-Oct-2020)

Ref Expression
Hypotheses uvtxnbgr.v 
|- V = ( Vtx ` G )
uvtxusgr.e 
|- E = ( Edg ` G )
Assertion uvtxusgrel 
|- ( G e. USGraph -> ( N e. ( UnivVtx ` G ) <-> ( N e. V /\ A. k e. ( V \ { N } ) { k , N } e. E ) ) )

Proof

Step Hyp Ref Expression
1 uvtxnbgr.v 
 |-  V = ( Vtx ` G )
2 uvtxusgr.e 
 |-  E = ( Edg ` G )
3 1 2 uvtxusgr 
 |-  ( G e. USGraph -> ( UnivVtx ` G ) = { v e. V | A. k e. ( V \ { v } ) { k , v } e. E } )
4 3 eleq2d 
 |-  ( G e. USGraph -> ( N e. ( UnivVtx ` G ) <-> N e. { v e. V | A. k e. ( V \ { v } ) { k , v } e. E } ) )
5 sneq 
 |-  ( v = N -> { v } = { N } )
6 5 difeq2d 
 |-  ( v = N -> ( V \ { v } ) = ( V \ { N } ) )
7 preq2 
 |-  ( v = N -> { k , v } = { k , N } )
8 7 eleq1d 
 |-  ( v = N -> ( { k , v } e. E <-> { k , N } e. E ) )
9 6 8 raleqbidv 
 |-  ( v = N -> ( A. k e. ( V \ { v } ) { k , v } e. E <-> A. k e. ( V \ { N } ) { k , N } e. E ) )
10 9 elrab 
 |-  ( N e. { v e. V | A. k e. ( V \ { v } ) { k , v } e. E } <-> ( N e. V /\ A. k e. ( V \ { N } ) { k , N } e. E ) )
11 4 10 bitrdi 
 |-  ( G e. USGraph -> ( N e. ( UnivVtx ` G ) <-> ( N e. V /\ A. k e. ( V \ { N } ) { k , N } e. E ) ) )