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=\mathrm{Vtx}\left(G\right)$$
Assertion	stgrnbgr0	$$⊢N\in {\mathbb{N}}_0\to G\mathrm{NeighbVtx}0=V\setminus \left\{0\right\}$$

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=\mathrm{Vtx}\left(G\right)$$
3	1 2	stgrvtx0	$$⊢N\in {\mathbb{N}}_0\to 0\in V$$
4		eqid	$$⊢\mathrm{Edg}\left(G\right)=\mathrm{Edg}\left(G\right)$$
5	2 4	dfnbgr2	$$⊢0\in V\to G\mathrm{NeighbVtx}0=\left\{x\in \left(V\setminus \left\{0\right\}\right)|\exists e\in \mathrm{Edg}\left(G\right)\left(0\in e\wedge x\in e\right)\right\}$$
6	3 5	syl	$$⊢N\in {\mathbb{N}}_0\to G\mathrm{NeighbVtx}0=\left\{x\in \left(V\setminus \left\{0\right\}\right)|\exists e\in \mathrm{Edg}\left(G\right)\left(0\in e\wedge x\in e\right)\right\}$$
7		eleq2	$$⊢e=\left\{0,x\right\}\to \left(0\in e\leftrightarrow 0\in \left\{0,x\right\}\right)$$
8		eleq2	$$⊢e=\left\{0,x\right\}\to \left(x\in e\leftrightarrow x\in \left\{0,x\right\}\right)$$
9	7 8	anbi12d	$$⊢e=\left\{0,x\right\}\to \left(\left(0\in e\wedge x\in e\right)\leftrightarrow \left(0\in \left\{0,x\right\}\wedge x\in \left\{0,x\right\}\right)\right)$$
10		0elfz	$$⊢N\in {\mathbb{N}}_0\to 0\in \left(0\dots N\right)$$
11	10	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \left(V\setminus \left\{0\right\}\right)\right)\to 0\in \left(0\dots N\right)$$
12		fz1ssfz0	$$⊢\left(1\dots N\right)\subseteq \left(0\dots N\right)$$
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\in {\mathbb{N}}_0\to V=\left(0\dots N\right)$$
17	16	difeq1d	$$⊢N\in {\mathbb{N}}_0\to V\setminus \left\{0\right\}=\left(0\dots N\right)\setminus \left\{0\right\}$$
18		fz0dif1	$$⊢N\in {\mathbb{N}}_0\to \left(0\dots N\right)\setminus \left\{0\right\}=\left(1\dots N\right)$$
19	18	eqimssd	$$⊢N\in {\mathbb{N}}_0\to \left(0\dots N\right)\setminus \left\{0\right\}\subseteq \left(1\dots N\right)$$
20	17 19	eqsstrd	$$⊢N\in {\mathbb{N}}_0\to V\setminus \left\{0\right\}\subseteq \left(1\dots N\right)$$
21	20	sselda	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \left(V\setminus \left\{0\right\}\right)\right)\to x\in \left(1\dots N\right)$$
22	12 21	sselid	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \left(V\setminus \left\{0\right\}\right)\right)\to x\in \left(0\dots N\right)$$
23	11 22	prssd	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \left(V\setminus \left\{0\right\}\right)\right)\to \left\{0,x\right\}\subseteq \left(0\dots N\right)$$
24		preq2	$$⊢n=x\to \left\{0,n\right\}=\left\{0,x\right\}$$
25	24	eqeq2d	$$⊢n=x\to \left(\left\{0,x\right\}=\left\{0,n\right\}\leftrightarrow \left\{0,x\right\}=\left\{0,x\right\}\right)$$
26		eqidd	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \left(V\setminus \left\{0\right\}\right)\right)\to \left\{0,x\right\}=\left\{0,x\right\}$$
27	25 21 26	rspcedvdw	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \left(V\setminus \left\{0\right\}\right)\right)\to \exists n\in \left(1\dots N\right)\left\{0,x\right\}=\left\{0,n\right\}$$
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	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \left(V\setminus \left\{0\right\}\right)\right)\to \left(\left\{0,x\right\}\in \mathrm{Edg}\left(G\right)\leftrightarrow \left(\left\{0,x\right\}\subseteq \left(0\dots N\right)\wedge \exists n\in \left(1\dots N\right)\left\{0,x\right\}=\left\{0,n\right\}\right)\right)$$
33	23 27 32	mpbir2and	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \left(V\setminus \left\{0\right\}\right)\right)\to \left\{0,x\right\}\in \mathrm{Edg}\left(G\right)$$
34		prid2g	$$⊢x\in \left(V\setminus \left\{0\right\}\right)\to x\in \left\{0,x\right\}$$
35	34	adantl	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \left(V\setminus \left\{0\right\}\right)\right)\to x\in \left\{0,x\right\}$$
36		c0ex	$$⊢0\in \mathrm{V}$$
37	36	prid1	$$⊢0\in \left\{0,x\right\}$$
38	35 37	jctil	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \left(V\setminus \left\{0\right\}\right)\right)\to \left(0\in \left\{0,x\right\}\wedge x\in \left\{0,x\right\}\right)$$
39	9 33 38	rspcedvdw	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \left(V\setminus \left\{0\right\}\right)\right)\to \exists e\in \mathrm{Edg}\left(G\right)\left(0\in e\wedge x\in e\right)$$
40	39	rabeqcda	$$⊢N\in {\mathbb{N}}_0\to \left\{x\in \left(V\setminus \left\{0\right\}\right)|\exists e\in \mathrm{Edg}\left(G\right)\left(0\in e\wedge x\in e\right)\right\}=V\setminus \left\{0\right\}$$
41	6 40	eqtrd	$$⊢N\in {\mathbb{N}}_0\to G\mathrm{NeighbVtx}0=V\setminus \left\{0\right\}$$