Metamath Proof Explorer

Theorem pgnbgreunbgrlem4

Description: Lemma 4 for pgnbgreunbgr . (Contributed by AV, 20-Nov-2025)

Ref Expression
Hypotheses pgnbgreunbgr.g 
|- G = ( 5 gPetersenGr 2 )
pgnbgreunbgr.v 
|- V = ( Vtx ` G )
pgnbgreunbgr.e 
|- E = ( Edg ` G )
pgnbgreunbgr.n 
|- N = ( G NeighbVtx X )
Assertion pgnbgreunbgrlem4 
|- ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ L = <. 0 , ( 2nd ` X ) >. \/ L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> ( ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ K = <. 0 , ( 2nd ` X ) >. \/ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> ( ( X e. V /\ X = <. 1 , y >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pgnbgreunbgr.g 
 |-  G = ( 5 gPetersenGr 2 )
2 pgnbgreunbgr.v 
 |-  V = ( Vtx ` G )
3 pgnbgreunbgr.e 
 |-  E = ( Edg ` G )
4 pgnbgreunbgr.n 
 |-  N = ( G NeighbVtx X )
5 1ex 
 |-  1 e. _V
6 vex 
 |-  y e. _V
7 5 6 op2ndd 
 |-  ( X = <. 1 , y >. -> ( 2nd ` X ) = y )
8 oveq1 
 |-  ( ( 2nd ` X ) = y -> ( ( 2nd ` X ) + 2 ) = ( y + 2 ) )
9 8 oveq1d 
 |-  ( ( 2nd ` X ) = y -> ( ( ( 2nd ` X ) + 2 ) mod 5 ) = ( ( y + 2 ) mod 5 ) )
10 9 opeq2d 
 |-  ( ( 2nd ` X ) = y -> <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. = <. 1 , ( ( y + 2 ) mod 5 ) >. )
11 10 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. <-> L = <. 1 , ( ( y + 2 ) mod 5 ) >. ) )
12 opeq2 
 |-  ( ( 2nd ` X ) = y -> <. 0 , ( 2nd ` X ) >. = <. 0 , y >. )
13 12 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( L = <. 0 , ( 2nd ` X ) >. <-> L = <. 0 , y >. ) )
14 oveq1 
 |-  ( ( 2nd ` X ) = y -> ( ( 2nd ` X ) - 2 ) = ( y - 2 ) )
15 14 oveq1d 
 |-  ( ( 2nd ` X ) = y -> ( ( ( 2nd ` X ) - 2 ) mod 5 ) = ( ( y - 2 ) mod 5 ) )
16 15 opeq2d 
 |-  ( ( 2nd ` X ) = y -> <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. = <. 1 , ( ( y - 2 ) mod 5 ) >. )
17 16 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. <-> L = <. 1 , ( ( y - 2 ) mod 5 ) >. ) )
18 11 13 17 3orbi123d 
 |-  ( ( 2nd ` X ) = y -> ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ L = <. 0 , ( 2nd ` X ) >. \/ L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) <-> ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. \/ L = <. 0 , y >. \/ L = <. 1 , ( ( y - 2 ) mod 5 ) >. ) ) )
19 10 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. <-> K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) )
20 12 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( K = <. 0 , ( 2nd ` X ) >. <-> K = <. 0 , y >. ) )
21 16 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. <-> K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) )
22 19 20 21 3orbi123d 
 |-  ( ( 2nd ` X ) = y -> ( ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ K = <. 0 , ( 2nd ` X ) >. \/ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) <-> ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. \/ K = <. 0 , y >. \/ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) ) )
23 18 22 anbi12d 
 |-  ( ( 2nd ` X ) = y -> ( ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ L = <. 0 , ( 2nd ` X ) >. \/ L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) /\ ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ K = <. 0 , ( 2nd ` X ) >. \/ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) ) <-> ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. \/ L = <. 0 , y >. \/ L = <. 1 , ( ( y - 2 ) mod 5 ) >. ) /\ ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. \/ K = <. 0 , y >. \/ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) ) ) )
24 simpr 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> K = <. 1 , ( ( y + 2 ) mod 5 ) >. )
25 simpl 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> L = <. 1 , ( ( y + 2 ) mod 5 ) >. )
26 24 25 neeq12d 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> ( K =/= L <-> <. 1 , ( ( y + 2 ) mod 5 ) >. =/= <. 1 , ( ( y + 2 ) mod 5 ) >. ) )
27 eqid 
 |-  <. 1 , ( ( y + 2 ) mod 5 ) >. = <. 1 , ( ( y + 2 ) mod 5 ) >.
28 eqneqall 
 |-  ( <. 1 , ( ( y + 2 ) mod 5 ) >. = <. 1 , ( ( y + 2 ) mod 5 ) >. -> ( <. 1 , ( ( y + 2 ) mod 5 ) >. =/= <. 1 , ( ( y + 2 ) mod 5 ) >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
29 27 28 ax-mp 
 |-  ( <. 1 , ( ( y + 2 ) mod 5 ) >. =/= <. 1 , ( ( y + 2 ) mod 5 ) >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
30 26 29 biimtrdi 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> ( K =/= L -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
31 30 impd 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
32 31 ex 
 |-  ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. -> ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
33 prcom 
 |-  { <. 1 , b >. , <. 0 , y >. } = { <. 0 , y >. , <. 1 , b >. }
34 33 eleq1i 
 |-  ( { <. 1 , b >. , <. 0 , y >. } e. E <-> { <. 0 , y >. , <. 1 , b >. } e. E )
35 5eluz3 
 |-  5 e. ( ZZ>= ` 3 )
36 pglem 
 |-  2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
37 eqid 
 |-  ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) = ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
38 eqid 
 |-  ( 0 ..^ 5 ) = ( 0 ..^ 5 )
39 37 38 1 3 gpgedgiov 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ ( y e. ( 0 ..^ 5 ) /\ b e. ( 0 ..^ 5 ) ) ) -> ( { <. 0 , y >. , <. 1 , b >. } e. E <-> y = b ) )
40 35 36 39 mpanl12 
 |-  ( ( y e. ( 0 ..^ 5 ) /\ b e. ( 0 ..^ 5 ) ) -> ( { <. 0 , y >. , <. 1 , b >. } e. E <-> y = b ) )
41 40 ancoms 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 0 , y >. , <. 1 , b >. } e. E <-> y = b ) )
42 34 41 bitrid 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 1 , b >. , <. 0 , y >. } e. E <-> y = b ) )
43 opeq2 
 |-  ( y = b -> <. 1 , y >. = <. 1 , b >. )
44 42 43 biimtrdi 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 1 , b >. , <. 0 , y >. } e. E -> <. 1 , y >. = <. 1 , b >. ) )
45 44 adantld 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 0 , y >. } e. E ) -> <. 1 , y >. = <. 1 , b >. ) )
46 preq1 
 |-  ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. -> { K , <. 1 , b >. } = { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 1 , b >. } )
47 46 eleq1d 
 |-  ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. -> ( { K , <. 1 , b >. } e. E <-> { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 1 , b >. } e. E ) )
48 preq2 
 |-  ( L = <. 0 , y >. -> { <. 1 , b >. , L } = { <. 1 , b >. , <. 0 , y >. } )
49 48 eleq1d 
 |-  ( L = <. 0 , y >. -> ( { <. 1 , b >. , L } e. E <-> { <. 1 , b >. , <. 0 , y >. } e. E ) )
50 47 49 bi2anan9r 
 |-  ( ( L = <. 0 , y >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) <-> ( { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 0 , y >. } e. E ) ) )
51 50 imbi1d 
 |-  ( ( L = <. 0 , y >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> ( ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) <-> ( ( { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 0 , y >. } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
52 45 51 imbitrrid 
 |-  ( ( L = <. 0 , y >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
53 52 adantld 
 |-  ( ( L = <. 0 , y >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
54 53 ex 
 |-  ( L = <. 0 , y >. -> ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
55 prcom 
 |-  { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 1 , b >. } = { <. 1 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. }
56 55 eleq1i 
 |-  ( { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 1 , b >. } e. E <-> { <. 1 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E )
57 prcom 
 |-  { <. 1 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } = { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. }
58 57 eleq1i 
 |-  ( { <. 1 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E <-> { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } e. E )
59 56 58 anbi12ci 
 |-  ( ( { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) <-> ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
60 5nn 
 |-  5 e. NN
61 60 nnzi 
 |-  5 e. ZZ
62 uzid 
 |-  ( 5 e. ZZ -> 5 e. ( ZZ>= ` 5 ) )
63 61 62 ax-mp 
 |-  5 e. ( ZZ>= ` 5 )
64 4t2e8 
 |-  ( 4 x. 2 ) = 8
65 64 oveq1i 
 |-  ( ( 4 x. 2 ) mod 5 ) = ( 8 mod 5 )
66 8mod5e3 
 |-  ( 8 mod 5 ) = 3
67 65 66 eqtri 
 |-  ( ( 4 x. 2 ) mod 5 ) = 3
68 3ne0 
 |-  3 =/= 0
69 67 68 eqnetri 
 |-  ( ( 4 x. 2 ) mod 5 ) =/= 0
70 36 69 pm3.2i 
 |-  ( 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) /\ ( ( 4 x. 2 ) mod 5 ) =/= 0 )
71 37 38 1 3 gpgedg2iv 
 |-  ( ( 5 e. ( ZZ>= ` 5 ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) /\ ( ( 4 x. 2 ) mod 5 ) =/= 0 ) ) -> ( ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) <-> b = y ) )
72 63 70 71 mp3an13 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) <-> b = y ) )
73 59 72 bitrid 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) <-> b = y ) )
74 43 eqcoms 
 |-  ( b = y -> <. 1 , y >. = <. 1 , b >. )
75 73 74 biimtrdi 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) -> <. 1 , y >. = <. 1 , b >. ) )
76 preq2 
 |-  ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. -> { <. 1 , b >. , L } = { <. 1 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } )
77 76 eleq1d 
 |-  ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. -> ( { <. 1 , b >. , L } e. E <-> { <. 1 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
78 47 77 bi2anan9r 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) <-> ( { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) ) )
79 78 imbi1d 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> ( ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) <-> ( ( { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
80 75 79 imbitrrid 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
81 80 adantld 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
82 81 ex 
 |-  ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. -> ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
83 32 54 82 3jaoi 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. \/ L = <. 0 , y >. \/ L = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
84 41 43 biimtrdi 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 0 , y >. , <. 1 , b >. } e. E -> <. 1 , y >. = <. 1 , b >. ) )
85 84 adantrd 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { <. 0 , y >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) -> <. 1 , y >. = <. 1 , b >. ) )
86 preq1 
 |-  ( K = <. 0 , y >. -> { K , <. 1 , b >. } = { <. 0 , y >. , <. 1 , b >. } )
87 86 eleq1d 
 |-  ( K = <. 0 , y >. -> ( { K , <. 1 , b >. } e. E <-> { <. 0 , y >. , <. 1 , b >. } e. E ) )
88 preq2 
 |-  ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. -> { <. 1 , b >. , L } = { <. 1 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } )
89 88 eleq1d 
 |-  ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. -> ( { <. 1 , b >. , L } e. E <-> { <. 1 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
90 87 89 bi2anan9r 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) <-> ( { <. 0 , y >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) )
91 90 imbi1d 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> ( ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) <-> ( ( { <. 0 , y >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
92 85 91 imbitrrid 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
93 92 adantld 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
94 93 ex 
 |-  ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. -> ( K = <. 0 , y >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
95 simpr 
 |-  ( ( L = <. 0 , y >. /\ K = <. 0 , y >. ) -> K = <. 0 , y >. )
96 simpl 
 |-  ( ( L = <. 0 , y >. /\ K = <. 0 , y >. ) -> L = <. 0 , y >. )
97 95 96 neeq12d 
 |-  ( ( L = <. 0 , y >. /\ K = <. 0 , y >. ) -> ( K =/= L <-> <. 0 , y >. =/= <. 0 , y >. ) )
98 eqid 
 |-  <. 0 , y >. = <. 0 , y >.
99 eqneqall 
 |-  ( <. 0 , y >. = <. 0 , y >. -> ( <. 0 , y >. =/= <. 0 , y >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
100 98 99 ax-mp 
 |-  ( <. 0 , y >. =/= <. 0 , y >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
101 97 100 biimtrdi 
 |-  ( ( L = <. 0 , y >. /\ K = <. 0 , y >. ) -> ( K =/= L -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
102 101 impd 
 |-  ( ( L = <. 0 , y >. /\ K = <. 0 , y >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
103 102 ex 
 |-  ( L = <. 0 , y >. -> ( K = <. 0 , y >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
104 84 adantrd 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { <. 0 , y >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) -> <. 1 , y >. = <. 1 , b >. ) )
105 86 adantl 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> { K , <. 1 , b >. } = { <. 0 , y >. , <. 1 , b >. } )
106 105 eleq1d 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> ( { K , <. 1 , b >. } e. E <-> { <. 0 , y >. , <. 1 , b >. } e. E ) )
107 76 adantr 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> { <. 1 , b >. , L } = { <. 1 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } )
108 107 eleq1d 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> ( { <. 1 , b >. , L } e. E <-> { <. 1 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
109 106 108 anbi12d 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) <-> ( { <. 0 , y >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) ) )
110 109 imbi1d 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> ( ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) <-> ( ( { <. 0 , y >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
111 104 110 imbitrrid 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
112 111 adantld 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
113 112 ex 
 |-  ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. -> ( K = <. 0 , y >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
114 94 103 113 3jaoi 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. \/ L = <. 0 , y >. \/ L = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( K = <. 0 , y >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
115 66 68 eqnetri 
 |-  ( 8 mod 5 ) =/= 0
116 65 115 eqnetri 
 |-  ( ( 4 x. 2 ) mod 5 ) =/= 0
117 simpll 
 |-  ( ( ( 5 e. ( ZZ>= ` 5 ) /\ ( ( 4 x. 2 ) mod 5 ) =/= 0 ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> 5 e. ( ZZ>= ` 5 ) )
118 simpr 
 |-  ( ( ( 5 e. ( ZZ>= ` 5 ) /\ ( ( 4 x. 2 ) mod 5 ) =/= 0 ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) )
119 36 a1i 
 |-  ( 5 e. ( ZZ>= ` 5 ) -> 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) )
120 119 anim1i 
 |-  ( ( 5 e. ( ZZ>= ` 5 ) /\ ( ( 4 x. 2 ) mod 5 ) =/= 0 ) -> ( 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) /\ ( ( 4 x. 2 ) mod 5 ) =/= 0 ) )
121 120 adantr 
 |-  ( ( ( 5 e. ( ZZ>= ` 5 ) /\ ( ( 4 x. 2 ) mod 5 ) =/= 0 ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) /\ ( ( 4 x. 2 ) mod 5 ) =/= 0 ) )
122 117 118 121 71 syl3anc 
 |-  ( ( ( 5 e. ( ZZ>= ` 5 ) /\ ( ( 4 x. 2 ) mod 5 ) =/= 0 ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) <-> b = y ) )
123 63 116 122 mpanl12 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) <-> b = y ) )
124 123 74 biimtrdi 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) -> <. 1 , y >. = <. 1 , b >. ) )
125 124 adantl 
 |-  ( ( <. 1 , ( ( y - 2 ) mod 5 ) >. =/= <. 1 , ( ( y + 2 ) mod 5 ) >. /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) -> <. 1 , y >. = <. 1 , b >. ) )
126 125 a1i 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( ( <. 1 , ( ( y - 2 ) mod 5 ) >. =/= <. 1 , ( ( y + 2 ) mod 5 ) >. /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
127 simpl 
 |-  ( ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ L = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> K = <. 1 , ( ( y - 2 ) mod 5 ) >. )
128 simpr 
 |-  ( ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ L = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> L = <. 1 , ( ( y + 2 ) mod 5 ) >. )
129 127 128 neeq12d 
 |-  ( ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ L = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> ( K =/= L <-> <. 1 , ( ( y - 2 ) mod 5 ) >. =/= <. 1 , ( ( y + 2 ) mod 5 ) >. ) )
130 129 ancoms 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( K =/= L <-> <. 1 , ( ( y - 2 ) mod 5 ) >. =/= <. 1 , ( ( y + 2 ) mod 5 ) >. ) )
131 130 anbi1d 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) <-> ( <. 1 , ( ( y - 2 ) mod 5 ) >. =/= <. 1 , ( ( y + 2 ) mod 5 ) >. /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) ) )
132 preq1 
 |-  ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. -> { K , <. 1 , b >. } = { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } )
133 132 eleq1d 
 |-  ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. -> ( { K , <. 1 , b >. } e. E <-> { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } e. E ) )
134 133 89 bi2anan9r 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) <-> ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) )
135 134 imbi1d 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) <-> ( ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
136 126 131 135 3imtr4d 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
137 136 ex 
 |-  ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. -> ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
138 39 ancom2s 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { <. 0 , y >. , <. 1 , b >. } e. E <-> y = b ) )
139 equcom 
 |-  ( y = b <-> b = y )
140 138 139 bitrdi 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { <. 0 , y >. , <. 1 , b >. } e. E <-> b = y ) )
141 34 140 bitrid 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { <. 1 , b >. , <. 0 , y >. } e. E <-> b = y ) )
142 35 36 141 mpanl12 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 1 , b >. , <. 0 , y >. } e. E <-> b = y ) )
143 142 74 biimtrdi 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 1 , b >. , <. 0 , y >. } e. E -> <. 1 , y >. = <. 1 , b >. ) )
144 143 adantld 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 0 , y >. } e. E ) -> <. 1 , y >. = <. 1 , b >. ) )
145 144 adantl 
 |-  ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 0 , y >. } e. E ) -> <. 1 , y >. = <. 1 , b >. ) )
146 132 adantl 
 |-  ( ( L = <. 0 , y >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> { K , <. 1 , b >. } = { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } )
147 146 eleq1d 
 |-  ( ( L = <. 0 , y >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( { K , <. 1 , b >. } e. E <-> { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } e. E ) )
148 49 adantr 
 |-  ( ( L = <. 0 , y >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( { <. 1 , b >. , L } e. E <-> { <. 1 , b >. , <. 0 , y >. } e. E ) )
149 147 148 anbi12d 
 |-  ( ( L = <. 0 , y >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) <-> ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 0 , y >. } e. E ) ) )
150 149 imbi1d 
 |-  ( ( L = <. 0 , y >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) <-> ( ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 1 , b >. } e. E /\ { <. 1 , b >. , <. 0 , y >. } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
151 145 150 imbitrrid 
 |-  ( ( L = <. 0 , y >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
152 151 ex 
 |-  ( L = <. 0 , y >. -> ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
153 eqeq2 
 |-  ( <. 1 , ( ( y - 2 ) mod 5 ) >. = L -> ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. <-> K = L ) )
154 153 eqcoms 
 |-  ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. -> ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. <-> K = L ) )
155 eqneqall 
 |-  ( K = L -> ( K =/= L -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
156 155 impd 
 |-  ( K = L -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
157 154 156 biimtrdi 
 |-  ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. -> ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
158 137 152 157 3jaoi 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. \/ L = <. 0 , y >. \/ L = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
159 83 114 158 3jaod 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. \/ L = <. 0 , y >. \/ L = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. \/ K = <. 0 , y >. \/ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
160 159 imp 
 |-  ( ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. \/ L = <. 0 , y >. \/ L = <. 1 , ( ( y - 2 ) mod 5 ) >. ) /\ ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. \/ K = <. 0 , y >. \/ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
161 23 160 biimtrdi 
 |-  ( ( 2nd ` X ) = y -> ( ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ L = <. 0 , ( 2nd ` X ) >. \/ L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) /\ ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ K = <. 0 , ( 2nd ` X ) >. \/ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
162 7 161 syl 
 |-  ( X = <. 1 , y >. -> ( ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ L = <. 0 , ( 2nd ` X ) >. \/ L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) /\ ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ K = <. 0 , ( 2nd ` X ) >. \/ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
163 eqeq1 
 |-  ( X = <. 1 , y >. -> ( X = <. 1 , b >. <-> <. 1 , y >. = <. 1 , b >. ) )
164 163 imbi2d 
 |-  ( X = <. 1 , y >. -> ( ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) <-> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) )
165 164 imbi2d 
 |-  ( X = <. 1 , y >. -> ( ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) <-> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> <. 1 , y >. = <. 1 , b >. ) ) ) )
166 162 165 sylibrd 
 |-  ( X = <. 1 , y >. -> ( ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ L = <. 0 , ( 2nd ` X ) >. \/ L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) /\ ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ K = <. 0 , ( 2nd ` X ) >. \/ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
167 166 adantl 
 |-  ( ( X e. V /\ X = <. 1 , y >. ) -> ( ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ L = <. 0 , ( 2nd ` X ) >. \/ L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) /\ ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ K = <. 0 , ( 2nd ` X ) >. \/ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
168 167 expdcom 
 |-  ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ L = <. 0 , ( 2nd ` X ) >. \/ L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> ( ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ K = <. 0 , ( 2nd ` X ) >. \/ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> ( ( X e. V /\ X = <. 1 , y >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) ) )