Metamath Proof Explorer

Theorem 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 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
gpgnbgr.g 
|- G = ( N gPetersenGr K )
gpgnbgr.v 
|- V = ( Vtx ` G )
gpgnbgr.u 
|- U = ( G NeighbVtx X )
gpgnbgr.e 
|- E = ( Edg ` G )
Assertion gpg5nbgrvtx03star 
|- ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( # ` U ) = 3 /\ A. x e. U A. y e. U { x , y } e/ E ) )

Proof

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