Theorem gpg5gricstgr3

Description: Each closed neighborhood in a generalized Petersen graph G(N,K) of order 10 ( N = 5 ), which is either the Petersen graph G(5,2) or the 5-prism G(5,1), is isomorphic to a 3-star. (Contributed by AV, 13-Sep-2025)

	Ref	Expression
Hypothesis	gpg5gricstgr3.g	No typesetting found for |- G = ( 5 gPetersenGr K ) with typecode |-
Assertion	gpg5gricstgr3	Could not format assertion : No typesetting found for |- ( ( K e. ( 1 ... 2 ) /\ V e. ( Vtx ` G ) ) -> ( G ISubGr ( G ClNeighbVtx V ) ) ~=gr ( StarGr ` 3 ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		gpg5gricstgr3.g	Could not format G = ( 5 gPetersenGr K ) : No typesetting found for |- G = ( 5 gPetersenGr K ) with typecode |-
2		5eluz3	$$⊢5\in {\mathbb{Z}}_{\ge 3}$$
3		2z	$$⊢2\in \mathbb{Z}$$
4		fzval3	$$⊢2\in \mathbb{Z}\to \left(1\dots 2\right)=\left(1..^2+1\right)$$
5	3 4	ax-mp	$$⊢\left(1\dots 2\right)=\left(1..^2+1\right)$$
6		2p1e3	$$⊢2+1=3$$
7	6	oveq2i	$$⊢\left(1..^2+1\right)=\left(1..^3\right)$$
8		ceil5half3	$$⊢⌈\frac{5}{2}⌉=3$$
9	8	eqcomi	$$⊢3=⌈\frac{5}{2}⌉$$
10	9	oveq2i	$$⊢\left(1..^3\right)=\left(1..^⌈\frac{5}{2}⌉\right)$$
11	5 7 10	3eqtri	$$⊢\left(1\dots 2\right)=\left(1..^⌈\frac{5}{2}⌉\right)$$
12	11	eleq2i	$$⊢K\in \left(1\dots 2\right)\leftrightarrow K\in \left(1..^⌈\frac{5}{2}⌉\right)$$
13	12	biimpi	$$⊢K\in \left(1\dots 2\right)\to K\in \left(1..^⌈\frac{5}{2}⌉\right)$$
14		gpgusgra	Could not format ( ( 5 e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr K ) e. USGraph ) : No typesetting found for |- ( ( 5 e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr K ) e. USGraph ) with typecode |-
15	1 14	eqeltrid	$$⊢\left(5\in {\mathbb{Z}}_{\ge 3}\wedge K\in \left(1..^⌈\frac{5}{2}⌉\right)\right)\to G\in \mathrm{USGraph}$$
16	2 13 15	sylancr	$$⊢K\in \left(1\dots 2\right)\to G\in \mathrm{USGraph}$$
17	16	anim1i	$$⊢\left(K\in \left(1\dots 2\right)\wedge V\in \mathrm{Vtx}\left(G\right)\right)\to \left(G\in \mathrm{USGraph}\wedge V\in \mathrm{Vtx}\left(G\right)\right)$$
18		eqidd	$$⊢\left(K\in \left(1\dots 2\right)\wedge V\in \mathrm{Vtx}\left(G\right)\right)\to 5=5$$
19	13	adantr	$$⊢\left(K\in \left(1\dots 2\right)\wedge V\in \mathrm{Vtx}\left(G\right)\right)\to K\in \left(1..^⌈\frac{5}{2}⌉\right)$$
20		simpr	$$⊢\left(K\in \left(1\dots 2\right)\wedge V\in \mathrm{Vtx}\left(G\right)\right)\to V\in \mathrm{Vtx}\left(G\right)$$
21		eqid	$$⊢\left(1..^⌈\frac{5}{2}⌉\right)=\left(1..^⌈\frac{5}{2}⌉\right)$$
22		eqid	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(G\right)$$
23		eqid	$$⊢G\mathrm{NeighbVtx}V=G\mathrm{NeighbVtx}V$$
24		eqid	$$⊢\mathrm{Edg}\left(G\right)=\mathrm{Edg}\left(G\right)$$
25	21 1 22 23 24	gpg5nbgr3star	$$⊢\left(5=5\wedge K\in \left(1..^⌈\frac{5}{2}⌉\right)\wedge V\in \mathrm{Vtx}\left(G\right)\right)\to \left(\left|G\mathrm{NeighbVtx}V\right|=3\wedge \forall x\in \left(G\mathrm{NeighbVtx}V\right)\forall y\in \left(G\mathrm{NeighbVtx}V\right)\left\{x,y\right\}\notin \mathrm{Edg}\left(G\right)\right)$$
26	18 19 20 25	syl3anc	$$⊢\left(K\in \left(1\dots 2\right)\wedge V\in \mathrm{Vtx}\left(G\right)\right)\to \left(\left|G\mathrm{NeighbVtx}V\right|=3\wedge \forall x\in \left(G\mathrm{NeighbVtx}V\right)\forall y\in \left(G\mathrm{NeighbVtx}V\right)\left\{x,y\right\}\notin \mathrm{Edg}\left(G\right)\right)$$
27		eqid	$$⊢GClNeighbVtxV=GClNeighbVtxV$$
28		3nn0	$$⊢3\in {\mathbb{N}}_0$$
29		eqid	Could not format ( StarGr ` 3 ) = ( StarGr ` 3 ) : No typesetting found for |- ( StarGr ` 3 ) = ( StarGr ` 3 ) with typecode |-
30		eqid	Could not format ( Vtx ` ( StarGr ` 3 ) ) = ( Vtx ` ( StarGr ` 3 ) ) : No typesetting found for |- ( Vtx ` ( StarGr ` 3 ) ) = ( Vtx ` ( StarGr ` 3 ) ) with typecode |-
31	22 23 27 28 29 30 24	isubgr3stgr	Could not format ( ( G e. USGraph /\ V e. ( Vtx ` G ) ) -> ( ( ( # ` ( G NeighbVtx V ) ) = 3 /\ A. x e. ( G NeighbVtx V ) A. y e. ( G NeighbVtx V ) { x , y } e/ ( Edg ` G ) ) -> ( G ISubGr ( G ClNeighbVtx V ) ) ~=gr ( StarGr ` 3 ) ) ) : No typesetting found for |- ( ( G e. USGraph /\ V e. ( Vtx ` G ) ) -> ( ( ( # ` ( G NeighbVtx V ) ) = 3 /\ A. x e. ( G NeighbVtx V ) A. y e. ( G NeighbVtx V ) { x , y } e/ ( Edg ` G ) ) -> ( G ISubGr ( G ClNeighbVtx V ) ) ~=gr ( StarGr ` 3 ) ) ) with typecode |-
32	17 26 31	sylc	Could not format ( ( K e. ( 1 ... 2 ) /\ V e. ( Vtx ` G ) ) -> ( G ISubGr ( G ClNeighbVtx V ) ) ~=gr ( StarGr ` 3 ) ) : No typesetting found for |- ( ( K e. ( 1 ... 2 ) /\ V e. ( Vtx ` G ) ) -> ( G ISubGr ( G ClNeighbVtx V ) ) ~=gr ( StarGr ` 3 ) ) with typecode |-