Metamath Proof Explorer

Theorem pgnbgreunbgrlem1

Description: Lemma 1 for pgnbgreunbgr . (Contributed by AV, 15-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 pgnbgreunbgrlem1 
|- ( ( L = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ L = <. 1 , ( 2nd ` X ) >. \/ L = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) -> ( ( K = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ K = <. 1 , ( 2nd ` X ) >. \/ K = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) -> ( ( X e. V /\ X = <. 0 , y >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , 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 c0ex 
 |-  0 e. _V
6 vex 
 |-  y e. _V
7 5 6 op2ndd 
 |-  ( X = <. 0 , y >. -> ( 2nd ` X ) = y )
8 oveq1 
 |-  ( ( 2nd ` X ) = y -> ( ( 2nd ` X ) + 1 ) = ( y + 1 ) )
9 8 oveq1d 
 |-  ( ( 2nd ` X ) = y -> ( ( ( 2nd ` X ) + 1 ) mod 5 ) = ( ( y + 1 ) mod 5 ) )
10 9 opeq2d 
 |-  ( ( 2nd ` X ) = y -> <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. = <. 0 , ( ( y + 1 ) mod 5 ) >. )
11 10 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( L = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. <-> L = <. 0 , ( ( y + 1 ) mod 5 ) >. ) )
12 opeq2 
 |-  ( ( 2nd ` X ) = y -> <. 1 , ( 2nd ` X ) >. = <. 1 , y >. )
13 12 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( L = <. 1 , ( 2nd ` X ) >. <-> L = <. 1 , y >. ) )
14 oveq1 
 |-  ( ( 2nd ` X ) = y -> ( ( 2nd ` X ) - 1 ) = ( y - 1 ) )
15 14 oveq1d 
 |-  ( ( 2nd ` X ) = y -> ( ( ( 2nd ` X ) - 1 ) mod 5 ) = ( ( y - 1 ) mod 5 ) )
16 15 opeq2d 
 |-  ( ( 2nd ` X ) = y -> <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. = <. 0 , ( ( y - 1 ) mod 5 ) >. )
17 16 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( L = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. <-> L = <. 0 , ( ( y - 1 ) mod 5 ) >. ) )
18 11 13 17 3orbi123d 
 |-  ( ( 2nd ` X ) = y -> ( ( L = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ L = <. 1 , ( 2nd ` X ) >. \/ L = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) <-> ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. \/ L = <. 1 , y >. \/ L = <. 0 , ( ( y - 1 ) mod 5 ) >. ) ) )
19 10 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( K = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. <-> K = <. 0 , ( ( y + 1 ) mod 5 ) >. ) )
20 12 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( K = <. 1 , ( 2nd ` X ) >. <-> K = <. 1 , y >. ) )
21 16 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( K = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. <-> K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) )
22 19 20 21 3orbi123d 
 |-  ( ( 2nd ` X ) = y -> ( ( K = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ K = <. 1 , ( 2nd ` X ) >. \/ K = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) <-> ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. \/ K = <. 1 , y >. \/ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) ) )
23 18 22 anbi12d 
 |-  ( ( 2nd ` X ) = y -> ( ( ( L = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ L = <. 1 , ( 2nd ` X ) >. \/ L = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) /\ ( K = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ K = <. 1 , ( 2nd ` X ) >. \/ K = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) ) <-> ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. \/ L = <. 1 , y >. \/ L = <. 0 , ( ( y - 1 ) mod 5 ) >. ) /\ ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. \/ K = <. 1 , y >. \/ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) ) ) )
24 simpr 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> K = <. 0 , ( ( y + 1 ) mod 5 ) >. )
25 simpl 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> L = <. 0 , ( ( y + 1 ) mod 5 ) >. )
26 24 25 neeq12d 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> ( K =/= L <-> <. 0 , ( ( y + 1 ) mod 5 ) >. =/= <. 0 , ( ( y + 1 ) mod 5 ) >. ) )
27 eqid 
 |-  <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 0 , ( ( y + 1 ) mod 5 ) >.
28 eqneqall 
 |-  ( <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( <. 0 , ( ( y + 1 ) mod 5 ) >. =/= <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
29 27 28 ax-mp 
 |-  ( <. 0 , ( ( y + 1 ) mod 5 ) >. =/= <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
30 26 29 biimtrdi 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> ( K =/= L -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
31 30 impd 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
32 31 ex 
 |-  ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
33 5eluz3 
 |-  5 e. ( ZZ>= ` 3 )
34 pglem 
 |-  2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
35 eqid 
 |-  ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) = ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
36 eqid 
 |-  ( 0 ..^ 5 ) = ( 0 ..^ 5 )
37 35 36 1 3 gpgedgiov 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { <. 0 , b >. , <. 1 , y >. } e. E <-> b = y ) )
38 33 34 37 mpanl12 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 0 , b >. , <. 1 , y >. } e. E <-> b = y ) )
39 opeq2 
 |-  ( y = b -> <. 0 , y >. = <. 0 , b >. )
40 39 eqcoms 
 |-  ( b = y -> <. 0 , y >. = <. 0 , b >. )
41 38 40 biimtrdi 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 0 , b >. , <. 1 , y >. } e. E -> <. 0 , y >. = <. 0 , b >. ) )
42 41 adantld 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { <. 0 , ( ( y + 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 1 , y >. } e. E ) -> <. 0 , y >. = <. 0 , b >. ) )
43 preq1 
 |-  ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. -> { K , <. 0 , b >. } = { <. 0 , ( ( y + 1 ) mod 5 ) >. , <. 0 , b >. } )
44 43 eleq1d 
 |-  ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( { K , <. 0 , b >. } e. E <-> { <. 0 , ( ( y + 1 ) mod 5 ) >. , <. 0 , b >. } e. E ) )
45 preq2 
 |-  ( L = <. 1 , y >. -> { <. 0 , b >. , L } = { <. 0 , b >. , <. 1 , y >. } )
46 45 eleq1d 
 |-  ( L = <. 1 , y >. -> ( { <. 0 , b >. , L } e. E <-> { <. 0 , b >. , <. 1 , y >. } e. E ) )
47 44 46 bi2anan9r 
 |-  ( ( L = <. 1 , y >. /\ K = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) <-> ( { <. 0 , ( ( y + 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 1 , y >. } e. E ) ) )
48 47 imbi1d 
 |-  ( ( L = <. 1 , y >. /\ K = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> ( ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) <-> ( ( { <. 0 , ( ( y + 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 1 , y >. } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
49 42 48 imbitrrid 
 |-  ( ( L = <. 1 , y >. /\ K = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
50 49 adantld 
 |-  ( ( L = <. 1 , y >. /\ K = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
51 50 ex 
 |-  ( L = <. 1 , y >. -> ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
52 prcom 
 |-  { <. 0 , ( ( y + 1 ) mod 5 ) >. , <. 0 , b >. } = { <. 0 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. }
53 52 eleq1i 
 |-  ( { <. 0 , ( ( y + 1 ) mod 5 ) >. , <. 0 , b >. } e. E <-> { <. 0 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
54 prcom 
 |-  { <. 0 , b >. , <. 0 , ( ( y - 1 ) mod 5 ) >. } = { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. }
55 54 eleq1i 
 |-  ( { <. 0 , b >. , <. 0 , ( ( y - 1 ) mod 5 ) >. } e. E <-> { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } e. E )
56 53 55 anbi12ci 
 |-  ( ( { <. 0 , ( ( y + 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y - 1 ) mod 5 ) >. } e. E ) <-> ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
57 5nn 
 |-  5 e. NN
58 57 nnzi 
 |-  5 e. ZZ
59 uzid 
 |-  ( 5 e. ZZ -> 5 e. ( ZZ>= ` 5 ) )
60 58 59 ax-mp 
 |-  5 e. ( ZZ>= ` 5 )
61 35 36 1 3 gpgedg2ov 
 |-  ( ( ( 5 e. ( ZZ>= ` 5 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) <-> b = y ) )
62 60 34 61 mpanl12 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) <-> b = y ) )
63 equcomiv 
 |-  ( b = y -> y = b )
64 63 opeq2d 
 |-  ( b = y -> <. 0 , y >. = <. 0 , b >. )
65 62 64 biimtrdi 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) -> <. 0 , y >. = <. 0 , b >. ) )
66 56 65 biimtrid 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { <. 0 , ( ( y + 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y - 1 ) mod 5 ) >. } e. E ) -> <. 0 , y >. = <. 0 , b >. ) )
67 preq2 
 |-  ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. -> { <. 0 , b >. , L } = { <. 0 , b >. , <. 0 , ( ( y - 1 ) mod 5 ) >. } )
68 67 eleq1d 
 |-  ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. -> ( { <. 0 , b >. , L } e. E <-> { <. 0 , b >. , <. 0 , ( ( y - 1 ) mod 5 ) >. } e. E ) )
69 44 68 bi2anan9r 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) <-> ( { <. 0 , ( ( y + 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y - 1 ) mod 5 ) >. } e. E ) ) )
70 69 imbi1d 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> ( ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) <-> ( ( { <. 0 , ( ( y + 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y - 1 ) mod 5 ) >. } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
71 66 70 imbitrrid 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
72 71 adantld 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
73 72 ex 
 |-  ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. -> ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
74 32 51 73 3jaoi 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. \/ L = <. 1 , y >. \/ L = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
75 prcom 
 |-  { <. 1 , y >. , <. 0 , b >. } = { <. 0 , b >. , <. 1 , y >. }
76 75 eleq1i 
 |-  ( { <. 1 , y >. , <. 0 , b >. } e. E <-> { <. 0 , b >. , <. 1 , y >. } e. E )
77 76 41 biimtrid 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 1 , y >. , <. 0 , b >. } e. E -> <. 0 , y >. = <. 0 , b >. ) )
78 77 adantrd 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { <. 1 , y >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) -> <. 0 , y >. = <. 0 , b >. ) )
79 preq1 
 |-  ( K = <. 1 , y >. -> { K , <. 0 , b >. } = { <. 1 , y >. , <. 0 , b >. } )
80 79 eleq1d 
 |-  ( K = <. 1 , y >. -> ( { K , <. 0 , b >. } e. E <-> { <. 1 , y >. , <. 0 , b >. } e. E ) )
81 preq2 
 |-  ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. -> { <. 0 , b >. , L } = { <. 0 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } )
82 81 eleq1d 
 |-  ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( { <. 0 , b >. , L } e. E <-> { <. 0 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
83 80 82 bi2anan9r 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) <-> ( { <. 1 , y >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) ) )
84 83 imbi1d 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) -> ( ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) <-> ( ( { <. 1 , y >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
85 78 84 imbitrrid 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
86 85 adantld 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
87 86 ex 
 |-  ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( K = <. 1 , y >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
88 simpr 
 |-  ( ( L = <. 1 , y >. /\ K = <. 1 , y >. ) -> K = <. 1 , y >. )
89 simpl 
 |-  ( ( L = <. 1 , y >. /\ K = <. 1 , y >. ) -> L = <. 1 , y >. )
90 88 89 neeq12d 
 |-  ( ( L = <. 1 , y >. /\ K = <. 1 , y >. ) -> ( K =/= L <-> <. 1 , y >. =/= <. 1 , y >. ) )
91 eqid 
 |-  <. 1 , y >. = <. 1 , y >.
92 eqneqall 
 |-  ( <. 1 , y >. = <. 1 , y >. -> ( <. 1 , y >. =/= <. 1 , y >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
93 91 92 ax-mp 
 |-  ( <. 1 , y >. =/= <. 1 , y >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
94 90 93 biimtrdi 
 |-  ( ( L = <. 1 , y >. /\ K = <. 1 , y >. ) -> ( K =/= L -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
95 94 impd 
 |-  ( ( L = <. 1 , y >. /\ K = <. 1 , y >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
96 95 ex 
 |-  ( L = <. 1 , y >. -> ( K = <. 1 , y >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
97 77 adantrd 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { <. 1 , y >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y - 1 ) mod 5 ) >. } e. E ) -> <. 0 , y >. = <. 0 , b >. ) )
98 79 adantl 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) -> { K , <. 0 , b >. } = { <. 1 , y >. , <. 0 , b >. } )
99 98 eleq1d 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) -> ( { K , <. 0 , b >. } e. E <-> { <. 1 , y >. , <. 0 , b >. } e. E ) )
100 67 adantr 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) -> { <. 0 , b >. , L } = { <. 0 , b >. , <. 0 , ( ( y - 1 ) mod 5 ) >. } )
101 100 eleq1d 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) -> ( { <. 0 , b >. , L } e. E <-> { <. 0 , b >. , <. 0 , ( ( y - 1 ) mod 5 ) >. } e. E ) )
102 99 101 anbi12d 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) <-> ( { <. 1 , y >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y - 1 ) mod 5 ) >. } e. E ) ) )
103 102 imbi1d 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) -> ( ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) <-> ( ( { <. 1 , y >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y - 1 ) mod 5 ) >. } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
104 97 103 imbitrrid 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
105 104 adantld 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
106 105 ex 
 |-  ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. -> ( K = <. 1 , y >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
107 87 96 106 3jaoi 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. \/ L = <. 1 , y >. \/ L = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( K = <. 1 , y >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
108 62 40 biimtrdi 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) -> <. 0 , y >. = <. 0 , b >. ) )
109 108 adantl 
 |-  ( ( <. 0 , ( ( y - 1 ) mod 5 ) >. =/= <. 0 , ( ( y + 1 ) mod 5 ) >. /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) -> <. 0 , y >. = <. 0 , b >. ) )
110 109 a1i 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( ( <. 0 , ( ( y - 1 ) mod 5 ) >. =/= <. 0 , ( ( y + 1 ) mod 5 ) >. /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
111 simpl 
 |-  ( ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ L = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> K = <. 0 , ( ( y - 1 ) mod 5 ) >. )
112 simpr 
 |-  ( ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ L = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> L = <. 0 , ( ( y + 1 ) mod 5 ) >. )
113 111 112 neeq12d 
 |-  ( ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ L = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> ( K =/= L <-> <. 0 , ( ( y - 1 ) mod 5 ) >. =/= <. 0 , ( ( y + 1 ) mod 5 ) >. ) )
114 113 ancoms 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( K =/= L <-> <. 0 , ( ( y - 1 ) mod 5 ) >. =/= <. 0 , ( ( y + 1 ) mod 5 ) >. ) )
115 114 anbi1d 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) <-> ( <. 0 , ( ( y - 1 ) mod 5 ) >. =/= <. 0 , ( ( y + 1 ) mod 5 ) >. /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) ) )
116 preq1 
 |-  ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. -> { K , <. 0 , b >. } = { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } )
117 116 eleq1d 
 |-  ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. -> ( { K , <. 0 , b >. } e. E <-> { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } e. E ) )
118 117 82 bi2anan9r 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) <-> ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) ) )
119 118 imbi1d 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) <-> ( ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
120 110 115 119 3imtr4d 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
121 120 ex 
 |-  ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
122 41 adantld 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 1 , y >. } e. E ) -> <. 0 , y >. = <. 0 , b >. ) )
123 122 adantl 
 |-  ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 1 , y >. } e. E ) -> <. 0 , y >. = <. 0 , b >. ) )
124 116 adantl 
 |-  ( ( L = <. 1 , y >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> { K , <. 0 , b >. } = { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } )
125 124 eleq1d 
 |-  ( ( L = <. 1 , y >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( { K , <. 0 , b >. } e. E <-> { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } e. E ) )
126 46 adantr 
 |-  ( ( L = <. 1 , y >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( { <. 0 , b >. , L } e. E <-> { <. 0 , b >. , <. 1 , y >. } e. E ) )
127 125 126 anbi12d 
 |-  ( ( L = <. 1 , y >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) <-> ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 1 , y >. } e. E ) ) )
128 127 imbi1d 
 |-  ( ( L = <. 1 , y >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) <-> ( ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 0 , b >. } e. E /\ { <. 0 , b >. , <. 1 , y >. } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
129 123 128 imbitrrid 
 |-  ( ( L = <. 1 , y >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
130 129 ex 
 |-  ( L = <. 1 , y >. -> ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
131 eqeq2 
 |-  ( <. 0 , ( ( y - 1 ) mod 5 ) >. = L -> ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. <-> K = L ) )
132 131 eqcoms 
 |-  ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. -> ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. <-> K = L ) )
133 eqneqall 
 |-  ( K = L -> ( K =/= L -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
134 133 impd 
 |-  ( K = L -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
135 132 134 biimtrdi 
 |-  ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. -> ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
136 121 130 135 3jaoi 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. \/ L = <. 1 , y >. \/ L = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
137 74 107 136 3jaod 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. \/ L = <. 1 , y >. \/ L = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. \/ K = <. 1 , y >. \/ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
138 137 imp 
 |-  ( ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. \/ L = <. 1 , y >. \/ L = <. 0 , ( ( y - 1 ) mod 5 ) >. ) /\ ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. \/ K = <. 1 , y >. \/ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
139 23 138 biimtrdi 
 |-  ( ( 2nd ` X ) = y -> ( ( ( L = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ L = <. 1 , ( 2nd ` X ) >. \/ L = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) /\ ( K = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ K = <. 1 , ( 2nd ` X ) >. \/ K = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
140 7 139 syl 
 |-  ( X = <. 0 , y >. -> ( ( ( L = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ L = <. 1 , ( 2nd ` X ) >. \/ L = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) /\ ( K = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ K = <. 1 , ( 2nd ` X ) >. \/ K = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
141 eqeq1 
 |-  ( X = <. 0 , y >. -> ( X = <. 0 , b >. <-> <. 0 , y >. = <. 0 , b >. ) )
142 141 imbi2d 
 |-  ( X = <. 0 , y >. -> ( ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) <-> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) )
143 142 imbi2d 
 |-  ( X = <. 0 , y >. -> ( ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) <-> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> <. 0 , y >. = <. 0 , b >. ) ) ) )
144 140 143 sylibrd 
 |-  ( X = <. 0 , y >. -> ( ( ( L = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ L = <. 1 , ( 2nd ` X ) >. \/ L = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) /\ ( K = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ K = <. 1 , ( 2nd ` X ) >. \/ K = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
145 144 adantl 
 |-  ( ( X e. V /\ X = <. 0 , y >. ) -> ( ( ( L = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ L = <. 1 , ( 2nd ` X ) >. \/ L = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) /\ ( K = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ K = <. 1 , ( 2nd ` X ) >. \/ K = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
146 145 expdcom 
 |-  ( ( L = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ L = <. 1 , ( 2nd ` X ) >. \/ L = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) -> ( ( K = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ K = <. 1 , ( 2nd ` X ) >. \/ K = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) -> ( ( X e. V /\ X = <. 0 , y >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )