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