Metamath Proof Explorer

Theorem stgrnbgr0

Description: All vertices of a star graph S_N except the center are in the (open) neighborhood of the center. (Contributed by AV, 12-Sep-2025)

Ref Expression
Hypotheses stgrvtx0.g 
|- G = ( StarGr ` N )
stgrvtx0.v 
|- V = ( Vtx ` G )
Assertion stgrnbgr0 
|- ( N e. NN0 -> ( G NeighbVtx 0 ) = ( V \ { 0 } ) )

Proof

Step Hyp Ref Expression
1 stgrvtx0.g 
 |-  G = ( StarGr ` N )
2 stgrvtx0.v 
 |-  V = ( Vtx ` G )
3 1 2 stgrvtx0 
 |-  ( N e. NN0 -> 0 e. V )
4 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
5 2 4 dfnbgr2 
 |-  ( 0 e. V -> ( G NeighbVtx 0 ) = { x e. ( V \ { 0 } ) | E. e e. ( Edg ` G ) ( 0 e. e /\ x e. e ) } )
6 3 5 syl 
 |-  ( N e. NN0 -> ( G NeighbVtx 0 ) = { x e. ( V \ { 0 } ) | E. e e. ( Edg ` G ) ( 0 e. e /\ x e. e ) } )
7 eleq2 
 |-  ( e = { 0 , x } -> ( 0 e. e <-> 0 e. { 0 , x } ) )
8 eleq2 
 |-  ( e = { 0 , x } -> ( x e. e <-> x e. { 0 , x } ) )
9 7 8 anbi12d 
 |-  ( e = { 0 , x } -> ( ( 0 e. e /\ x e. e ) <-> ( 0 e. { 0 , x } /\ x e. { 0 , x } ) ) )
10 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
11 10 adantr 
 |-  ( ( N e. NN0 /\ x e. ( V \ { 0 } ) ) -> 0 e. ( 0 ... N ) )
12 fz1ssfz0 
 |-  ( 1 ... N ) C_ ( 0 ... N )
13 1 fveq2i 
 |-  ( Vtx ` G ) = ( Vtx ` ( StarGr ` N ) )
14 2 13 eqtri 
 |-  V = ( Vtx ` ( StarGr ` N ) )
15 stgrvtx 
 |-  ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) )
16 14 15 eqtrid 
 |-  ( N e. NN0 -> V = ( 0 ... N ) )
17 16 difeq1d 
 |-  ( N e. NN0 -> ( V \ { 0 } ) = ( ( 0 ... N ) \ { 0 } ) )
18 fz0dif1 
 |-  ( N e. NN0 -> ( ( 0 ... N ) \ { 0 } ) = ( 1 ... N ) )
19 18 eqimssd 
 |-  ( N e. NN0 -> ( ( 0 ... N ) \ { 0 } ) C_ ( 1 ... N ) )
20 17 19 eqsstrd 
 |-  ( N e. NN0 -> ( V \ { 0 } ) C_ ( 1 ... N ) )
21 20 sselda 
 |-  ( ( N e. NN0 /\ x e. ( V \ { 0 } ) ) -> x e. ( 1 ... N ) )
22 12 21 sselid 
 |-  ( ( N e. NN0 /\ x e. ( V \ { 0 } ) ) -> x e. ( 0 ... N ) )
23 11 22 prssd 
 |-  ( ( N e. NN0 /\ x e. ( V \ { 0 } ) ) -> { 0 , x } C_ ( 0 ... N ) )
24 preq2 
 |-  ( n = x -> { 0 , n } = { 0 , x } )
25 24 eqeq2d 
 |-  ( n = x -> ( { 0 , x } = { 0 , n } <-> { 0 , x } = { 0 , x } ) )
26 eqidd 
 |-  ( ( N e. NN0 /\ x e. ( V \ { 0 } ) ) -> { 0 , x } = { 0 , x } )
27 25 21 26 rspcedvdw 
 |-  ( ( N e. NN0 /\ x e. ( V \ { 0 } ) ) -> E. n e. ( 1 ... N ) { 0 , x } = { 0 , n } )
28 1 fveq2i 
 |-  ( Edg ` G ) = ( Edg ` ( StarGr ` N ) )
29 28 eleq2i 
 |-  ( { 0 , x } e. ( Edg ` G ) <-> { 0 , x } e. ( Edg ` ( StarGr ` N ) ) )
30 stgredgel 
 |-  ( N e. NN0 -> ( { 0 , x } e. ( Edg ` ( StarGr ` N ) ) <-> ( { 0 , x } C_ ( 0 ... N ) /\ E. n e. ( 1 ... N ) { 0 , x } = { 0 , n } ) ) )
31 30 adantr 
 |-  ( ( N e. NN0 /\ x e. ( V \ { 0 } ) ) -> ( { 0 , x } e. ( Edg ` ( StarGr ` N ) ) <-> ( { 0 , x } C_ ( 0 ... N ) /\ E. n e. ( 1 ... N ) { 0 , x } = { 0 , n } ) ) )
32 29 31 bitrid 
 |-  ( ( N e. NN0 /\ x e. ( V \ { 0 } ) ) -> ( { 0 , x } e. ( Edg ` G ) <-> ( { 0 , x } C_ ( 0 ... N ) /\ E. n e. ( 1 ... N ) { 0 , x } = { 0 , n } ) ) )
33 23 27 32 mpbir2and 
 |-  ( ( N e. NN0 /\ x e. ( V \ { 0 } ) ) -> { 0 , x } e. ( Edg ` G ) )
34 prid2g 
 |-  ( x e. ( V \ { 0 } ) -> x e. { 0 , x } )
35 34 adantl 
 |-  ( ( N e. NN0 /\ x e. ( V \ { 0 } ) ) -> x e. { 0 , x } )
36 c0ex 
 |-  0 e. _V
37 36 prid1 
 |-  0 e. { 0 , x }
38 35 37 jctil 
 |-  ( ( N e. NN0 /\ x e. ( V \ { 0 } ) ) -> ( 0 e. { 0 , x } /\ x e. { 0 , x } ) )
39 9 33 38 rspcedvdw 
 |-  ( ( N e. NN0 /\ x e. ( V \ { 0 } ) ) -> E. e e. ( Edg ` G ) ( 0 e. e /\ x e. e ) )
40 39 rabeqcda 
 |-  ( N e. NN0 -> { x e. ( V \ { 0 } ) | E. e e. ( Edg ` G ) ( 0 e. e /\ x e. e ) } = ( V \ { 0 } ) )
41 6 40 eqtrd 
 |-  ( N e. NN0 -> ( G NeighbVtx 0 ) = ( V \ { 0 } ) )