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 No typesetting found for |- G = ( StarGr ` N ) with typecode |-
stgrvtx0.v V = Vtx G
Assertion stgrnbgr0 N 0 G NeighbVtx 0 = V 0

Proof

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