gpg5nbgrvtx03star

Description: In a generalized Petersen graph G(N,K) of order greater than 8 ( 3 < N ), every vertex of the first kind has exactly three (different) neighbors, and none of these neighbors are connected by an edge (i.e., the (closed) neighborhood of every vertex of the first kind induces a subgraph which is isomorphic to a 3-star). (Contributed by AV, 31-Aug-2025)

	Ref	Expression
Hypotheses	gpgnbgr.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
	gpgnbgr.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
	gpgnbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	gpgnbgr.u	⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
	gpgnbgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	gpg5nbgrvtx03star	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		gpgnbgr.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2		gpgnbgr.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
3		gpgnbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
4		gpgnbgr.u	⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
5		gpgnbgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
6		eluz4eluz3	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) → 𝑁 ∈ ( ℤ_≥ ‘ 3 ) )
7	1 2 3 4	gpg3nbgrvtx0	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ♯ ‘ 𝑈 ) = 3 )
8	6 7	sylanl1	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ♯ ‘ 𝑈 ) = 3 )
9		eqid	⊢ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩
10	1	eleq2i	⊢ ( 𝐾 ∈ 𝐽 ↔ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
11	10	biimpi	⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
12		gpgusgra	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 𝑁 gPetersenGr 𝐾 ) ∈ USGraph )
13	2 12	eqeltrid	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → 𝐺 ∈ USGraph )
14	6 11 13	syl2an	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) → 𝐺 ∈ USGraph )
15	14	adantr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 𝐺 ∈ USGraph )
16	5	usgredgne	⊢ ( ( 𝐺 ∈ USGraph ∧ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ )
17	16	neneqd	⊢ ( ( 𝐺 ∈ USGraph ∧ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ¬ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ )
18	17	ex	⊢ ( 𝐺 ∈ USGraph → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → ¬ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ) )
19	15 18	syl	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → ¬ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ) )
20	9 19	mt2i	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ¬ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 )
21		df-nel	⊢ ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ↔ ¬ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 )
22	20 21	sylibr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
23	6	adantr	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) → 𝑁 ∈ ( ℤ_≥ ‘ 3 ) )
24	23	adantr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 𝑁 ∈ ( ℤ_≥ ‘ 3 ) )
25		simplr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 𝐾 ∈ 𝐽 )
26	6	anim1i	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) )
27		simpl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) → 𝑋 ∈ 𝑉 )
28	26 27	anim12i	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) )
29		eqid	⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
30	29 1 2 3	gpgvtxel2	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ( 2^nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) )
31	28 30	syl	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( 2^nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) )
32	1 2 3 5	gpg5nbgrvtx03starlem1	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ ( 2^nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) ) → { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 )
33	24 25 31 32	syl3anc	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 )
34		simpll	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 𝑁 ∈ ( ℤ_≥ ‘ 4 ) )
35		elfzoelz	⊢ ( ( 2^nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) → ( 2^nd ‘ 𝑋 ) ∈ ℤ )
36	28 30 35	3syl	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( 2^nd ‘ 𝑋 ) ∈ ℤ )
37	1 2 3 5	gpg5nbgrvtx03starlem2	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ∧ ( 2^nd ‘ 𝑋 ) ∈ ℤ ) → { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
38	34 25 36 37	syl3anc	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
39		opex	⊢ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ V
40		opex	⊢ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ V
41		opex	⊢ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ V
42		preq2	⊢ ( 𝑦 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ → { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } )
43		neleq1	⊢ ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
44	42 43	syl	⊢ ( 𝑦 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
45		preq2	⊢ ( 𝑦 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ → { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } )
46		neleq1	⊢ ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ) )
47	45 46	syl	⊢ ( 𝑦 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ) )
48		preq2	⊢ ( 𝑦 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ → { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } )
49		neleq1	⊢ ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
50	48 49	syl	⊢ ( 𝑦 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
51	39 40 41 44 47 50	raltp	⊢ ( ∀ 𝑦 ∈ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ∧ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ∧ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
52	22 33 38 51	syl3anbrc	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ∀ 𝑦 ∈ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 )
53		prcom	⊢ { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ }
54		neleq1	⊢ ( { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } → ( { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ) )
55	53 54	ax-mp	⊢ ( { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 )
56	33 55	sylibr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
57		eqid	⊢ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩
58	5	usgredgne	⊢ ( ( 𝐺 ∈ USGraph ∧ { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ) → ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ≠ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ )
59	58	neneqd	⊢ ( ( 𝐺 ∈ USGraph ∧ { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ) → ¬ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ )
60	59	ex	⊢ ( 𝐺 ∈ USGraph → ( { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 → ¬ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ) )
61	15 60	syl	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 → ¬ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ) )
62	57 61	mt2i	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ¬ { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 )
63		df-nel	⊢ ( { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ↔ ¬ { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 )
64	62 63	sylibr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 )
65	1 2 3 5	gpg5nbgrvtx03starlem3	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ ( 2^nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) ) → { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
66	24 25 31 65	syl3anc	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
67		preq2	⊢ ( 𝑦 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ → { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } = { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } )
68		neleq1	⊢ ( { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } = { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } → ( { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
69	67 68	syl	⊢ ( 𝑦 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ → ( { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
70		preq2	⊢ ( 𝑦 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ → { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } = { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } )
71		neleq1	⊢ ( { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } = { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } → ( { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ) )
72	70 71	syl	⊢ ( 𝑦 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ → ( { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ) )
73		preq2	⊢ ( 𝑦 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ → { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } = { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } )
74		neleq1	⊢ ( { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } = { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } → ( { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
75	73 74	syl	⊢ ( 𝑦 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ → ( { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
76	39 40 41 69 72 75	raltp	⊢ ( ∀ 𝑦 ∈ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ ( { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ∧ { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ∧ { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
77	56 64 66 76	syl3anbrc	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ∀ 𝑦 ∈ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 )
78		prcom	⊢ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ }
79		neleq1	⊢ ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
80	78 79	ax-mp	⊢ ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
81	38 80	sylibr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
82		prcom	⊢ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } = { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ }
83		neleq1	⊢ ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } = { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ↔ { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
84	82 83	ax-mp	⊢ ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ↔ { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
85	66 84	sylibr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 )
86		eqid	⊢ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩
87	5	usgredgne	⊢ ( ( 𝐺 ∈ USGraph ∧ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ )
88	87	neneqd	⊢ ( ( 𝐺 ∈ USGraph ∧ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ¬ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ )
89	88	ex	⊢ ( 𝐺 ∈ USGraph → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → ¬ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ) )
90	15 89	syl	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → ¬ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ) )
91	86 90	mt2i	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ¬ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 )
92		df-nel	⊢ ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ↔ ¬ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 )
93	91 92	sylibr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
94		preq2	⊢ ( 𝑦 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ → { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } )
95		neleq1	⊢ ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
96	94 95	syl	⊢ ( 𝑦 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
97		preq2	⊢ ( 𝑦 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ → { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } )
98		neleq1	⊢ ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ) )
99	97 98	syl	⊢ ( 𝑦 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ) )
100		preq2	⊢ ( 𝑦 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ → { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } )
101		neleq1	⊢ ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
102	100 101	syl	⊢ ( 𝑦 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ → ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
103	39 40 41 96 99 102	raltp	⊢ ( ∀ 𝑦 ∈ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ ( { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ∧ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ∧ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
104	81 85 93 103	syl3anbrc	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ∀ 𝑦 ∈ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 )
105		preq1	⊢ ( 𝑥 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ → { 𝑥 , 𝑦 } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } )
106		neleq1	⊢ ( { 𝑥 , 𝑦 } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } → ( { 𝑥 , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
107	105 106	syl	⊢ ( 𝑥 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ → ( { 𝑥 , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
108	107	ralbidv	⊢ ( 𝑥 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ → ( ∀ 𝑦 ∈ { ⟨ 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 𝑁 ) ⟩ } { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
109		preq1	⊢ ( 𝑥 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ → { 𝑥 , 𝑦 } = { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } )
110		neleq1	⊢ ( { 𝑥 , 𝑦 } = { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } → ( { 𝑥 , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
111	109 110	syl	⊢ ( 𝑥 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ → ( { 𝑥 , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
112	111	ralbidv	⊢ ( 𝑥 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ → ( ∀ 𝑦 ∈ { ⟨ 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 𝑁 ) ⟩ } { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
113		preq1	⊢ ( 𝑥 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ → { 𝑥 , 𝑦 } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } )
114		neleq1	⊢ ( { 𝑥 , 𝑦 } = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } → ( { 𝑥 , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
115	113 114	syl	⊢ ( 𝑥 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ → ( { 𝑥 , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
116	115	ralbidv	⊢ ( 𝑥 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ → ( ∀ 𝑦 ∈ { ⟨ 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 𝑁 ) ⟩ } { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
117	39 40 41 108 112 116	raltp	⊢ ( ∀ 𝑥 ∈ { ⟨ 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 𝑁 ) ⟩ } { 𝑥 , 𝑦 } ∉ 𝐸 ↔ ( ∀ 𝑦 ∈ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ∧ ∀ 𝑦 ∈ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } { ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ∧ ∀ 𝑦 ∈ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
118	52 77 104 117	syl3anbrc	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ∀ 𝑥 ∈ { ⟨ 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 𝑁 ) ⟩ } { 𝑥 , 𝑦 } ∉ 𝐸 )
119	1 2 3 4	gpgnbgrvtx0	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 𝑈 = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } )
120	6 119	sylanl1	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 𝑈 = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } )
121	120	raleqdv	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ↔ ∀ 𝑦 ∈ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } { 𝑥 , 𝑦 } ∉ 𝐸 ) )
122	120 121	raleqbidvv	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ↔ ∀ 𝑥 ∈ { ⟨ 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 𝑁 ) ⟩ } { 𝑥 , 𝑦 } ∉ 𝐸 ) )
123	118 122	mpbird	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 )
124	8 123	jca	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) )

Metamath Proof Explorer

Theorem gpg5nbgrvtx03star

Proof