gpgnbgrvtx0

Description: The (open) neighborhood of an outside vertex in a generalized Petersen graph G . (Contributed by AV, 28-Aug-2025)

	Ref	Expression
Hypotheses	gpgnbgr.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
	gpgnbgr.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
	gpgnbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	gpgnbgr.u	⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
Assertion	gpgnbgrvtx0	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 𝑈 = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		gpgnbgr.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2		gpgnbgr.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
3		gpgnbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
4		gpgnbgr.u	⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
5	4	a1i	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 𝑈 = ( 𝐺 NeighbVtx 𝑋 ) )
6	1	eleq2i	⊢ ( 𝐾 ∈ 𝐽 ↔ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
7		gpgusgra	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 𝑁 gPetersenGr 𝐾 ) ∈ USGraph )
8	6 7	sylan2b	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑁 gPetersenGr 𝐾 ) ∈ USGraph )
9	2 8	eqeltrid	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝐺 ∈ USGraph )
10		simpl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) → 𝑋 ∈ 𝑉 )
11		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
12	3 11	nbusgrvtx	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑋 ) = { 𝑦 ∈ 𝑉 ∣ { 𝑋 , 𝑦 } ∈ ( Edg ‘ 𝐺 ) } )
13	9 10 12	syl2an	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( 𝐺 NeighbVtx 𝑋 ) = { 𝑦 ∈ 𝑉 ∣ { 𝑋 , 𝑦 } ∈ ( Edg ‘ 𝐺 ) } )
14		simpl	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) )
15		simpr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) → ( 1^st ‘ 𝑋 ) = 0 )
16	15	adantl	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( 1^st ‘ 𝑋 ) = 0 )
17		simpr	⊢ ( ( 𝑣 ∈ 𝑉 ∧ { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) → { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) )
18	1 2 3 11	gpgvtxedg0	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 0 ∧ { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∨ 𝑣 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ) )
19	14 16 17 18	syl2an3an	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∨ 𝑣 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ) )
20	19	ex	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( 𝑣 ∈ 𝑉 ∧ { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∨ 𝑣 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ) ) )
21	1 2 3	gpgvtx0	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ( ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
22	21	simp1d	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 )
23	22	adantrr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 )
24	1 2 3 11	gpgedgvtx0	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( { 𝑋 , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑋 , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑋 , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) ) )
25	24	simp1d	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → { 𝑋 , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) )
26	23 25	jca	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ { 𝑋 , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) ) )
27		eleq1	⊢ ( 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ → ( 𝑣 ∈ 𝑉 ↔ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
28		preq2	⊢ ( 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ → { 𝑋 , 𝑣 } = { 𝑋 , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } )
29	28	eleq1d	⊢ ( 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ → ( { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝑋 , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) ) )
30	27 29	anbi12d	⊢ ( 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ → ( ( 𝑣 ∈ 𝑉 ∧ { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ { 𝑋 , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) ) ) )
31	26 30	syl5ibrcom	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ → ( 𝑣 ∈ 𝑉 ∧ { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) )
32	1 2 3	gpgvtx1	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
33	32	simp2d	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 )
34	33	adantrr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 )
35	24	simp2d	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → { 𝑋 , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) )
36	34 35	jca	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ { 𝑋 , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) ) )
37		eleq1	⊢ ( 𝑣 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ → ( 𝑣 ∈ 𝑉 ↔ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ) )
38		preq2	⊢ ( 𝑣 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ → { 𝑋 , 𝑣 } = { 𝑋 , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } )
39	38	eleq1d	⊢ ( 𝑣 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ → ( { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝑋 , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) ) )
40	37 39	anbi12d	⊢ ( 𝑣 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ → ( ( 𝑣 ∈ 𝑉 ∧ { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ { 𝑋 , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) ) ) )
41	36 40	syl5ibrcom	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( 𝑣 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ → ( 𝑣 ∈ 𝑉 ∧ { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) )
42	21	simp3d	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 )
43	42	adantrr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 )
44	43	adantr	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) ∧ 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ) → ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 )
45		eleq1	⊢ ( 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ → ( 𝑣 ∈ 𝑉 ↔ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
46	45	adantl	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) ∧ 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ) → ( 𝑣 ∈ 𝑉 ↔ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
47	44 46	mpbird	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) ∧ 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ) → 𝑣 ∈ 𝑉 )
48	24	simp3d	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → { 𝑋 , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) )
49	48	adantr	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) ∧ 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ) → { 𝑋 , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) )
50		preq2	⊢ ( 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ → { 𝑋 , 𝑣 } = { 𝑋 , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } )
51	50	eleq1d	⊢ ( 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ → ( { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝑋 , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) ) )
52	51	adantl	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) ∧ 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ) → ( { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝑋 , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) ) )
53	49 52	mpbird	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) ∧ 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ) → { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) )
54	47 53	jca	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) ∧ 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ) → ( 𝑣 ∈ 𝑉 ∧ { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) )
55	54	ex	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ → ( 𝑣 ∈ 𝑉 ∧ { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) )
56	31 41 55	3jaod	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∨ 𝑣 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ) → ( 𝑣 ∈ 𝑉 ∧ { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) )
57	20 56	impbid	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( 𝑣 ∈ 𝑉 ∧ { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∨ 𝑣 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ) ) )
58		preq2	⊢ ( 𝑦 = 𝑣 → { 𝑋 , 𝑦 } = { 𝑋 , 𝑣 } )
59	58	eleq1d	⊢ ( 𝑦 = 𝑣 → ( { 𝑋 , 𝑦 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) )
60	59	elrab	⊢ ( 𝑣 ∈ { 𝑦 ∈ 𝑉 ∣ { 𝑋 , 𝑦 } ∈ ( Edg ‘ 𝐺 ) } ↔ ( 𝑣 ∈ 𝑉 ∧ { 𝑋 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) )
61		vex	⊢ 𝑣 ∈ V
62	61	eltp	⊢ ( 𝑣 ∈ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ↔ ( 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∨ 𝑣 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑣 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ) )
63	57 60 62	3bitr4g	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( 𝑣 ∈ { 𝑦 ∈ 𝑉 ∣ { 𝑋 , 𝑦 } ∈ ( Edg ‘ 𝐺 ) } ↔ 𝑣 ∈ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ) )
64	63	eqrdv	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → { 𝑦 ∈ 𝑉 ∣ { 𝑋 , 𝑦 } ∈ ( Edg ‘ 𝐺 ) } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } )
65	5 13 64	3eqtrd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 𝑈 = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } )

Metamath Proof Explorer

Theorem gpgnbgrvtx0

Proof