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 syl5bb
 |-  ( ( 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 }