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

Metamath Proof Explorer

Theorem isuvtx

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

Ref Expression
Hypotheses uvtxel.v 
|- V = ( Vtx ` G )
isuvtx.e 
|- E = ( Edg ` G )
Assertion isuvtx 
|- ( UnivVtx ` G ) = { v e. V | A. k e. ( V \ { v } ) E. e e. E { k , v } C_ e }

Proof

Step Hyp Ref Expression
1 uvtxel.v 
 |-  V = ( Vtx ` G )
2 isuvtx.e 
 |-  E = ( Edg ` G )
3 1 uvtxval 
 |-  ( UnivVtx ` G ) = { v e. V | A. k e. ( V \ { v } ) k e. ( G NeighbVtx v ) }
4 1 2 nbgrel 
 |-  ( k e. ( G NeighbVtx v ) <-> ( ( k e. V /\ v e. V ) /\ k =/= v /\ E. e e. E { v , k } C_ e ) )
5 df-3an 
 |-  ( ( ( k e. V /\ v e. V ) /\ k =/= v /\ E. e e. E { v , k } C_ e ) <-> ( ( ( k e. V /\ v e. V ) /\ k =/= v ) /\ E. e e. E { v , k } C_ e ) )
6 4 5 bitri 
 |-  ( k e. ( G NeighbVtx v ) <-> ( ( ( k e. V /\ v e. V ) /\ k =/= v ) /\ E. e e. E { v , k } C_ e ) )
7 prcom 
 |-  { k , v } = { v , k }
8 7 sseq1i 
 |-  ( { k , v } C_ e <-> { v , k } C_ e )
9 8 rexbii 
 |-  ( E. e e. E { k , v } C_ e <-> E. e e. E { v , k } C_ e )
10 id 
 |-  ( v e. V -> v e. V )
11 eldifi 
 |-  ( k e. ( V \ { v } ) -> k e. V )
12 10 11 anim12ci 
 |-  ( ( v e. V /\ k e. ( V \ { v } ) ) -> ( k e. V /\ v e. V ) )
13 eldifsni 
 |-  ( k e. ( V \ { v } ) -> k =/= v )
14 13 adantl 
 |-  ( ( v e. V /\ k e. ( V \ { v } ) ) -> k =/= v )
15 12 14 jca 
 |-  ( ( v e. V /\ k e. ( V \ { v } ) ) -> ( ( k e. V /\ v e. V ) /\ k =/= v ) )
16 15 biantrurd 
 |-  ( ( v e. V /\ k e. ( V \ { v } ) ) -> ( E. e e. E { v , k } C_ e <-> ( ( ( k e. V /\ v e. V ) /\ k =/= v ) /\ E. e e. E { v , k } C_ e ) ) )
17 9 16 bitr2id 
 |-  ( ( v e. V /\ k e. ( V \ { v } ) ) -> ( ( ( ( k e. V /\ v e. V ) /\ k =/= v ) /\ E. e e. E { v , k } C_ e ) <-> E. e e. E { k , v } C_ e ) )
18 6 17 bitrid 
 |-  ( ( v e. V /\ k e. ( V \ { v } ) ) -> ( k e. ( G NeighbVtx v ) <-> E. e e. E { k , v } C_ e ) )
19 18 ralbidva 
 |-  ( v e. V -> ( A. k e. ( V \ { v } ) k e. ( G NeighbVtx v ) <-> A. k e. ( V \ { v } ) E. e e. E { k , v } C_ e ) )
20 19 rabbiia 
 |-  { v e. V | A. k e. ( V \ { v } ) k e. ( G NeighbVtx v ) } = { v e. V | A. k e. ( V \ { v } ) E. e e. E { k , v } C_ e }
21 3 20 eqtri 
 |-  ( UnivVtx ` G ) = { v e. V | A. k e. ( V \ { v } ) E. e e. E { k , v } C_ e }