Metamath Proof Explorer

Theorem gpg5nbgr3star

Description: In a generalized Petersen graph G(N,K) of order 10 ( N = 5 ), these are the Petersen graph G(5,2) and the 5-prism G(5,1), every vertex has exactly three (different) neighbors, and none of these neighbors are connected by an edge (i.e., the (closed) neighborhood of every vertex induces a subgraph which is isomorphic to a 3-star). This does not hold for every generalized Petersen graph: for example, in the 3-prism G(3,1) (see gpg31grim3prism TODO) and the Dürer graph G(6,2) there are vertices which have neighborhoods containing triangles. In general, all generalized Peterson graphs G(N,K) with N = 3 x. K contain triangles, see gpg3kgrtriex . (Contributed by AV, 8-Sep-2025)

Ref Expression
Hypotheses gpgnbgr.j ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
gpgnbgr.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
gpgnbgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
gpgnbgr.u ⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
gpgnbgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion gpg5nbgr3star ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( ( ♯ ‘ 𝑈 ) = 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 5eluz3 ⊢ 5 ∈ ( ℤ≥ ‘ 3 )
7 eleq1 ⊢ ( 𝑁 = 5 → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ↔ 5 ∈ ( ℤ≥ ‘ 3 ) ) )
8 6 7 mpbiri ⊢ ( 𝑁 = 5 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
9 8 anim1i ⊢ ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) )
10 eqid ⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
11 10 1 2 3 gpgvtxel ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑎 ∈ { 0 , 1 } ∃ 𝑏 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ) )
12 9 11 syl ⊢ ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑎 ∈ { 0 , 1 } ∃ 𝑏 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ) )
13 12 biimp3a ⊢ ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑎 ∈ { 0 , 1 } ∃ 𝑏 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ )
14 elpri ⊢ ( 𝑎 ∈ { 0 , 1 } → ( 𝑎 = 0 ∨ 𝑎 = 1 ) )
15 opeq1 ⊢ ( 𝑎 = 0 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 0 , 𝑏 ⟩ )
16 15 eqeq2d ⊢ ( 𝑎 = 0 → ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑋 = ⟨ 0 , 𝑏 ⟩ ) )
17 16 adantr ⊢ ( ( 𝑎 = 0 ∧ ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑋 = ⟨ 0 , 𝑏 ⟩ ) )
18 c0ex ⊢ 0 ∈ V
19 vex ⊢ 𝑏 ∈ V
20 18 19 op1std ⊢ ( 𝑋 = ⟨ 0 , 𝑏 ⟩ → ( 1st ‘ 𝑋 ) = 0 )
21 4z ⊢ 4 ∈ ℤ
22 5nn ⊢ 5 ∈ ℕ
23 22 nnzi ⊢ 5 ∈ ℤ
24 4re ⊢ 4 ∈ ℝ
25 5re ⊢ 5 ∈ ℝ
26 4lt5 ⊢ 4 < 5
27 24 25 26 ltleii ⊢ 4 ≤ 5
28 eluz2 ⊢ ( 5 ∈ ( ℤ≥ ‘ 4 ) ↔ ( 4 ∈ ℤ ∧ 5 ∈ ℤ ∧ 4 ≤ 5 ) )
29 21 23 27 28 mpbir3an ⊢ 5 ∈ ( ℤ≥ ‘ 4 )
30 eleq1 ⊢ ( 𝑁 = 5 → ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ↔ 5 ∈ ( ℤ≥ ‘ 4 ) ) )
31 29 30 mpbiri ⊢ ( 𝑁 = 5 → 𝑁 ∈ ( ℤ≥ ‘ 4 ) )
32 1 2 3 4 5 gpg5nbgrvtx03star ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) )
33 31 32 sylanl1 ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) )
34 33 exp43 ⊢ ( 𝑁 = 5 → ( 𝐾 ∈ 𝐽 → ( 𝑋 ∈ 𝑉 → ( ( 1st ‘ 𝑋 ) = 0 → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ) ) )
35 34 3imp ⊢ ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( ( 1st ‘ 𝑋 ) = 0 → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) )
36 20 35 syl5 ⊢ ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 = ⟨ 0 , 𝑏 ⟩ → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) )
37 36 adantl ⊢ ( ( 𝑎 = 0 ∧ ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑋 = ⟨ 0 , 𝑏 ⟩ → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) )
38 17 37 sylbid ⊢ ( ( 𝑎 = 0 ∧ ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) )
39 38 ex ⊢ ( 𝑎 = 0 → ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ) )
40 opeq1 ⊢ ( 𝑎 = 1 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 1 , 𝑏 ⟩ )
41 40 eqeq2d ⊢ ( 𝑎 = 1 → ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
42 41 adantr ⊢ ( ( 𝑎 = 1 ∧ ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
43 1ex ⊢ 1 ∈ V
44 43 19 op1std ⊢ ( 𝑋 = ⟨ 1 , 𝑏 ⟩ → ( 1st ‘ 𝑋 ) = 1 )
45 1 2 3 4 gpg3nbgrvtx1 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ♯ ‘ 𝑈 ) = 3 )
46 8 45 sylanl1 ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ♯ ‘ 𝑈 ) = 3 )
47 eqid ⊢ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩
48 1 eleq2i ⊢ ( 𝐾 ∈ 𝐽 ↔ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
49 48 biimpi ⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
50 gpgusgra ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 𝑁 gPetersenGr 𝐾 ) ∈ USGraph )
51 2 50 eqeltrid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → 𝐺 ∈ USGraph )
52 8 49 51 syl2an ⊢ ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) → 𝐺 ∈ USGraph )
53 52 adantr ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → 𝐺 ∈ USGraph )
54 5 usgredgne ⊢ ( ( 𝐺 ∈ USGraph ∧ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ )
55 54 neneqd ⊢ ( ( 𝐺 ∈ USGraph ∧ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ¬ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ )
56 55 ex ⊢ ( 𝐺 ∈ USGraph → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → ¬ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ) )
57 53 56 syl ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → ¬ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ) )
58 47 57 mt2i ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ¬ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 )
59 df-nel ⊢ ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ↔ ¬ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 )
60 58 59 sylibr ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
61 fvexd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) → ( 2nd ‘ 𝑋 ) ∈ V )
62 1 2 3 5 gpg5nbgrvtx13starlem1 ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 2nd ‘ 𝑋 ) ∈ V ) → { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 )
63 61 62 sylan2 ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 )
64 simpl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) → 𝑋 ∈ 𝑉 )
65 9 64 anim12i ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) )
66 10 1 2 3 gpgvtxel2 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ( 2nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) )
67 elfzoelz ⊢ ( ( 2nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) → ( 2nd ‘ 𝑋 ) ∈ ℤ )
68 65 66 67 3syl ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( 2nd ‘ 𝑋 ) ∈ ℤ )
69 1 2 3 5 gpg5nbgrvtx13starlem2 ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 2nd ‘ 𝑋 ) ∈ ℤ ) → { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
70 68 69 syldan ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
71 opex ⊢ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ V
72 opex ⊢ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ V
73 opex ⊢ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ V
74 preq2 ⊢ ( 𝑦 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ → { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } )
75 neleq1 ⊢ ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
76 74 75 syl ⊢ ( 𝑦 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
77 preq2 ⊢ ( 𝑦 = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ → { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } )
78 neleq1 ⊢ ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ) )
79 77 78 syl ⊢ ( 𝑦 = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ) )
80 preq2 ⊢ ( 𝑦 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ → { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } )
81 neleq1 ⊢ ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
82 80 81 syl ⊢ ( 𝑦 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
83 71 72 73 76 79 82 raltp ⊢ ( ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ∧ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ∧ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
84 60 63 70 83 syl3anbrc ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 )
85 prcom ⊢ { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ }
86 neleq1 ⊢ ( { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } → ( { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ) )
87 85 86 ax-mp ⊢ ( { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 )
88 63 87 sylibr ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
89 eqid ⊢ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩
90 5 usgredgne ⊢ ( ( 𝐺 ∈ USGraph ∧ { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ) → ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ≠ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ )
91 90 neneqd ⊢ ( ( 𝐺 ∈ USGraph ∧ { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ) → ¬ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ )
92 91 ex ⊢ ( 𝐺 ∈ USGraph → ( { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 → ¬ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ) )
93 53 92 syl ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 → ¬ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ) )
94 89 93 mt2i ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ¬ { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 )
95 df-nel ⊢ ( { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ↔ ¬ { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 )
96 94 95 sylibr ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 )
97 1 2 3 5 gpg5nbgrvtx13starlem3 ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 2nd ‘ 𝑋 ) ∈ V ) → { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
98 61 97 sylan2 ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
99 preq2 ⊢ ( 𝑦 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ → { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } = { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } )
100 neleq1 ⊢ ( { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } = { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } → ( { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
101 99 100 syl ⊢ ( 𝑦 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ → ( { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
102 preq2 ⊢ ( 𝑦 = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ → { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } = { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } )
103 neleq1 ⊢ ( { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } = { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } → ( { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ) )
104 102 103 syl ⊢ ( 𝑦 = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ → ( { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ) )
105 preq2 ⊢ ( 𝑦 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ → { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } = { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } )
106 neleq1 ⊢ ( { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } = { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } → ( { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
107 105 106 syl ⊢ ( 𝑦 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ → ( { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
108 71 72 73 101 104 107 raltp ⊢ ( ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ ( { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ∧ { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ∧ { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
109 88 96 98 108 syl3anbrc ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 )
110 prcom ⊢ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ }
111 neleq1 ⊢ ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
112 110 111 ax-mp ⊢ ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
113 70 112 sylibr ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
114 prcom ⊢ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } = { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ }
115 neleq1 ⊢ ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } = { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ↔ { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
116 114 115 ax-mp ⊢ ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ↔ { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
117 98 116 sylibr ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 )
118 eqid ⊢ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩
119 5 usgredgne ⊢ ( ( 𝐺 ∈ USGraph ∧ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ )
120 119 neneqd ⊢ ( ( 𝐺 ∈ USGraph ∧ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ¬ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ )
121 120 ex ⊢ ( 𝐺 ∈ USGraph → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → ¬ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) )
122 53 121 syl ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → ¬ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) )
123 118 122 mt2i ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ¬ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 )
124 df-nel ⊢ ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ↔ ¬ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 )
125 123 124 sylibr ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 )
126 preq2 ⊢ ( 𝑦 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ → { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } )
127 neleq1 ⊢ ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
128 126 127 syl ⊢ ( 𝑦 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
129 preq2 ⊢ ( 𝑦 = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ → { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } )
130 neleq1 ⊢ ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ) )
131 129 130 syl ⊢ ( 𝑦 = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ) )
132 preq2 ⊢ ( 𝑦 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ → { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } )
133 neleq1 ⊢ ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
134 132 133 syl ⊢ ( 𝑦 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ → ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
135 71 72 73 128 131 134 raltp ⊢ ( ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ↔ ( { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ∧ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∉ 𝐸 ∧ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∉ 𝐸 ) )
136 113 117 125 135 syl3anbrc ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 )
137 preq1 ⊢ ( 𝑥 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ → { 𝑥 , 𝑦 } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } )
138 neleq1 ⊢ ( { 𝑥 , 𝑦 } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } → ( { 𝑥 , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
139 137 138 syl ⊢ ( 𝑥 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ → ( { 𝑥 , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
140 139 ralbidv ⊢ ( 𝑥 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ → ( ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { 𝑥 , 𝑦 } ∉ 𝐸 ↔ ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
141 preq1 ⊢ ( 𝑥 = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ → { 𝑥 , 𝑦 } = { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } )
142 neleq1 ⊢ ( { 𝑥 , 𝑦 } = { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } → ( { 𝑥 , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
143 141 142 syl ⊢ ( 𝑥 = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ → ( { 𝑥 , 𝑦 } ∉ 𝐸 ↔ { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
144 143 ralbidv ⊢ ( 𝑥 = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ → ( ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { 𝑥 , 𝑦 } ∉ 𝐸 ↔ ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
145 preq1 ⊢ ( 𝑥 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ → { 𝑥 , 𝑦 } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } )
146 neleq1 ⊢ ( { 𝑥 , 𝑦 } = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } → ( { 𝑥 , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
147 145 146 syl ⊢ ( 𝑥 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ → ( { 𝑥 , 𝑦 } ∉ 𝐸 ↔ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
148 147 ralbidv ⊢ ( 𝑥 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ → ( ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { 𝑥 , 𝑦 } ∉ 𝐸 ↔ ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
149 71 72 73 140 144 148 raltp ⊢ ( ∀ 𝑥 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { 𝑥 , 𝑦 } ∉ 𝐸 ↔ ( ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ∧ ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , 𝑦 } ∉ 𝐸 ∧ ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ , 𝑦 } ∉ 𝐸 ) )
150 84 109 136 149 syl3anbrc ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ∀ 𝑥 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { 𝑥 , 𝑦 } ∉ 𝐸 )
151 1 2 3 4 gpgnbgrvtx1 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → 𝑈 = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } )
152 8 151 sylanl1 ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → 𝑈 = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } )
153 152 raleqdv ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ↔ ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { 𝑥 , 𝑦 } ∉ 𝐸 ) )
154 152 153 raleqbidv ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ↔ ∀ 𝑥 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∀ 𝑦 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } { 𝑥 , 𝑦 } ∉ 𝐸 ) )
155 150 154 mpbird ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 )
156 46 155 jca ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) )
157 156 exp43 ⊢ ( 𝑁 = 5 → ( 𝐾 ∈ 𝐽 → ( 𝑋 ∈ 𝑉 → ( ( 1st ‘ 𝑋 ) = 1 → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ) ) )
158 157 3imp ⊢ ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( ( 1st ‘ 𝑋 ) = 1 → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) )
159 44 158 syl5 ⊢ ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 = ⟨ 1 , 𝑏 ⟩ → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) )
160 159 adantl ⊢ ( ( 𝑎 = 1 ∧ ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑋 = ⟨ 1 , 𝑏 ⟩ → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) )
161 42 160 sylbid ⊢ ( ( 𝑎 = 1 ∧ ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) )
162 161 ex ⊢ ( 𝑎 = 1 → ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ) )
163 39 162 jaoi ⊢ ( ( 𝑎 = 0 ∨ 𝑎 = 1 ) → ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ) )
164 14 163 syl ⊢ ( 𝑎 ∈ { 0 , 1 } → ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ) )
165 164 impcom ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑎 ∈ { 0 , 1 } ) → ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) )
166 165 a1d ⊢ ( ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑎 ∈ { 0 , 1 } ) → ( 𝑏 ∈ ( 0 ..^ 𝑁 ) → ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ) )
167 166 expimpd ⊢ ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑎 ∈ { 0 , 1 } ∧ 𝑏 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ) )
168 167 rexlimdvv ⊢ ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( ∃ 𝑎 ∈ { 0 , 1 } ∃ 𝑏 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) )
169 13 168 mpd ⊢ ( ( 𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( ( ♯ ‘ 𝑈 ) = 3 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) )