Metamath Proof Explorer

Theorem pgnbgreunbgrlem5

Description: Lemma 5 for pgnbgreunbgr . Impossible cases. (Contributed by AV, 21-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 pgnbgreunbgrlem5 
|- ( ( 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 = <. 0 , y >. /\ X e. V ) -> ( ( 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 c0ex 
 |-  0 e. _V
6 vex 
 |-  y e. _V
7 5 6 op2ndd 
 |-  ( X = <. 0 , y >. -> ( 2nd ` X ) = y )
8 7 adantr 
 |-  ( ( X = <. 0 , y >. /\ X e. V ) -> ( 2nd ` X ) = y )
9 oveq1 
 |-  ( ( 2nd ` X ) = y -> ( ( 2nd ` X ) + 1 ) = ( y + 1 ) )
10 9 oveq1d 
 |-  ( ( 2nd ` X ) = y -> ( ( ( 2nd ` X ) + 1 ) mod 5 ) = ( ( y + 1 ) mod 5 ) )
11 10 opeq2d 
 |-  ( ( 2nd ` X ) = y -> <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. = <. 0 , ( ( y + 1 ) mod 5 ) >. )
12 11 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( L = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. <-> L = <. 0 , ( ( y + 1 ) mod 5 ) >. ) )
13 opeq2 
 |-  ( ( 2nd ` X ) = y -> <. 1 , ( 2nd ` X ) >. = <. 1 , y >. )
14 13 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( L = <. 1 , ( 2nd ` X ) >. <-> L = <. 1 , y >. ) )
15 oveq1 
 |-  ( ( 2nd ` X ) = y -> ( ( 2nd ` X ) - 1 ) = ( y - 1 ) )
16 15 oveq1d 
 |-  ( ( 2nd ` X ) = y -> ( ( ( 2nd ` X ) - 1 ) mod 5 ) = ( ( y - 1 ) mod 5 ) )
17 16 opeq2d 
 |-  ( ( 2nd ` X ) = y -> <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. = <. 0 , ( ( y - 1 ) mod 5 ) >. )
18 17 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( L = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. <-> L = <. 0 , ( ( y - 1 ) mod 5 ) >. ) )
19 12 14 18 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 ) >. ) ) )
20 11 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( K = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. <-> K = <. 0 , ( ( y + 1 ) mod 5 ) >. ) )
21 13 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( K = <. 1 , ( 2nd ` X ) >. <-> K = <. 1 , y >. ) )
22 17 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( K = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. <-> K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) )
23 20 21 22 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 ) >. ) ) )
24 19 23 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 ) >. ) ) ) )
25 8 24 syl 
 |-  ( ( X = <. 0 , y >. /\ X e. V ) -> ( ( ( 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 ) >. ) ) ) )
26 simpl 
 |-  ( ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ L = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> K = <. 0 , ( ( y + 1 ) mod 5 ) >. )
27 simpr 
 |-  ( ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ L = <. 0 , ( ( y + 1 ) mod 5 ) >. ) -> L = <. 0 , ( ( y + 1 ) mod 5 ) >. )
28 26 27 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 ) >. ) )
29 28 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 ) >. ) )
30 eqid 
 |-  <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 0 , ( ( y + 1 ) mod 5 ) >.
31 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
32 30 31 ax-mp 
 |-  ( <. 0 , ( ( y + 1 ) mod 5 ) >. =/= <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) )
33 29 32 biimtrdi 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y + 1 ) 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 >. ) ) ) )
34 33 impd 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y + 1 ) 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 >. ) ) )
35 34 ex 
 |-  ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( K = <. 0 , ( ( y + 1 ) 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 >. ) ) ) )
36 1 2 3 4 pgnbgreunbgrlem5lem1 
 |-  ( ( ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { K , <. 1 , b >. } e. E ) -> -. { <. 1 , b >. , L } e. E )
37 36 pm2.21d 
 |-  ( ( ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { K , <. 1 , b >. } e. E ) -> ( { <. 1 , b >. , L } e. E -> X = <. 1 , b >. ) )
38 37 expimpd 
 |-  ( ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) )
39 38 ex 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) )
40 39 adantld 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 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 >. ) ) )
41 40 ex 
 |-  ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( K = <. 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 >. ) ) ) )
42 1 2 3 4 pgnbgreunbgrlem5lem3 
 |-  ( ( ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { K , <. 1 , b >. } e. E ) -> -. { <. 1 , b >. , L } e. E )
43 42 pm2.21d 
 |-  ( ( ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { K , <. 1 , b >. } e. E ) -> ( { <. 1 , b >. , L } e. E -> X = <. 1 , b >. ) )
44 43 expimpd 
 |-  ( ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) )
45 44 ex 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) )
46 45 adantld 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) 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 >. ) ) )
47 46 ex 
 |-  ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( K = <. 0 , ( ( y - 1 ) 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 >. ) ) ) )
48 35 41 47 3jaod 
 |-  ( 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
49 prcom 
 |-  { K , <. 1 , b >. } = { <. 1 , b >. , K }
50 49 eleq1i 
 |-  ( { K , <. 1 , b >. } e. E <-> { <. 1 , b >. , K } e. E )
51 prcom 
 |-  { <. 1 , b >. , L } = { L , <. 1 , b >. }
52 51 eleq1i 
 |-  ( { <. 1 , b >. , L } e. E <-> { L , <. 1 , b >. } e. E )
53 50 52 anbi12i 
 |-  ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) <-> ( { <. 1 , b >. , K } e. E /\ { L , <. 1 , b >. } e. E ) )
54 1 2 3 4 pgnbgreunbgrlem5lem1 
 |-  ( ( ( ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ L = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { L , <. 1 , b >. } e. E ) -> -. { <. 1 , b >. , K } e. E )
55 54 pm2.21d 
 |-  ( ( ( ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ L = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { L , <. 1 , b >. } e. E ) -> ( { <. 1 , b >. , K } e. E -> X = <. 1 , b >. ) )
56 55 ex 
 |-  ( ( ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ L = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { L , <. 1 , b >. } e. E -> ( { <. 1 , b >. , K } e. E -> X = <. 1 , b >. ) ) )
57 56 impcomd 
 |-  ( ( ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ L = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { <. 1 , b >. , K } e. E /\ { L , <. 1 , b >. } e. E ) -> X = <. 1 , b >. ) )
58 53 57 biimtrid 
 |-  ( ( ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ L = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) )
59 58 ex 
 |-  ( ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ L = <. 1 , y >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) )
60 59 adantld 
 |-  ( ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ L = <. 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 >. ) ) )
61 60 expcom 
 |-  ( L = <. 1 , y >. -> ( K = <. 0 , ( ( y + 1 ) 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 >. ) ) ) )
62 simpr 
 |-  ( ( L = <. 1 , y >. /\ K = <. 1 , y >. ) -> K = <. 1 , y >. )
63 simpl 
 |-  ( ( L = <. 1 , y >. /\ K = <. 1 , y >. ) -> L = <. 1 , y >. )
64 62 63 neeq12d 
 |-  ( ( L = <. 1 , y >. /\ K = <. 1 , y >. ) -> ( K =/= L <-> <. 1 , y >. =/= <. 1 , y >. ) )
65 eqid 
 |-  <. 1 , y >. = <. 1 , y >.
66 eqneqall 
 |-  ( <. 1 , y >. = <. 1 , y >. -> ( <. 1 , y >. =/= <. 1 , y >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
67 65 66 ax-mp 
 |-  ( <. 1 , y >. =/= <. 1 , y >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) )
68 64 67 biimtrdi 
 |-  ( ( L = <. 1 , y >. /\ K = <. 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 >. ) ) ) )
69 68 impd 
 |-  ( ( L = <. 1 , y >. /\ K = <. 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 >. ) ) )
70 69 ex 
 |-  ( L = <. 1 , y >. -> ( K = <. 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 >. ) ) ) )
71 1 2 3 4 pgnbgreunbgrlem5lem2 
 |-  ( ( ( ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ L = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { L , <. 1 , b >. } e. E ) -> -. { <. 1 , b >. , K } e. E )
72 71 pm2.21d 
 |-  ( ( ( ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ L = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { L , <. 1 , b >. } e. E ) -> ( { <. 1 , b >. , K } e. E -> X = <. 1 , b >. ) )
73 72 ex 
 |-  ( ( ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ L = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { L , <. 1 , b >. } e. E -> ( { <. 1 , b >. , K } e. E -> X = <. 1 , b >. ) ) )
74 73 impcomd 
 |-  ( ( ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ L = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { <. 1 , b >. , K } e. E /\ { L , <. 1 , b >. } e. E ) -> X = <. 1 , b >. ) )
75 53 74 biimtrid 
 |-  ( ( ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ L = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) )
76 75 ex 
 |-  ( ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ L = <. 1 , y >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) )
77 76 adantld 
 |-  ( ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ L = <. 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 >. ) ) )
78 77 expcom 
 |-  ( L = <. 1 , y >. -> ( K = <. 0 , ( ( y - 1 ) 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 >. ) ) ) )
79 61 70 78 3jaod 
 |-  ( L = <. 1 , y >. -> ( ( 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
80 1 2 3 4 pgnbgreunbgrlem5lem3 
 |-  ( ( ( ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ L = <. 0 , ( ( y - 1 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { L , <. 1 , b >. } e. E ) -> -. { <. 1 , b >. , K } e. E )
81 80 pm2.21d 
 |-  ( ( ( ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ L = <. 0 , ( ( y - 1 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { L , <. 1 , b >. } e. E ) -> ( { <. 1 , b >. , K } e. E -> X = <. 1 , b >. ) )
82 81 ex 
 |-  ( ( ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ L = <. 0 , ( ( y - 1 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { L , <. 1 , b >. } e. E -> ( { <. 1 , b >. , K } e. E -> X = <. 1 , b >. ) ) )
83 82 impcomd 
 |-  ( ( ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ L = <. 0 , ( ( y - 1 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { <. 1 , b >. , K } e. E /\ { L , <. 1 , b >. } e. E ) -> X = <. 1 , b >. ) )
84 53 83 biimtrid 
 |-  ( ( ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ L = <. 0 , ( ( y - 1 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) )
85 84 ex 
 |-  ( ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ L = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) )
86 85 adantld 
 |-  ( ( K = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ L = <. 0 , ( ( y - 1 ) 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 >. ) ) )
87 86 expcom 
 |-  ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. -> ( K = <. 0 , ( ( y + 1 ) 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 >. ) ) ) )
88 1 2 3 4 pgnbgreunbgrlem5lem2 
 |-  ( ( ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { K , <. 1 , b >. } e. E ) -> -. { <. 1 , b >. , L } e. E )
89 88 pm2.21d 
 |-  ( ( ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { K , <. 1 , b >. } e. E ) -> ( { <. 1 , b >. , L } e. E -> X = <. 1 , b >. ) )
90 89 expimpd 
 |-  ( ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) )
91 90 ex 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) )
92 91 adantld 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 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 >. ) ) )
93 92 ex 
 |-  ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. -> ( K = <. 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 >. ) ) ) )
94 simpr 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> K = <. 0 , ( ( y - 1 ) mod 5 ) >. )
95 simpl 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> L = <. 0 , ( ( y - 1 ) mod 5 ) >. )
96 94 95 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 ) >. ) )
97 eqid 
 |-  <. 0 , ( ( y - 1 ) mod 5 ) >. = <. 0 , ( ( y - 1 ) mod 5 ) >.
98 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
99 97 98 ax-mp 
 |-  ( <. 0 , ( ( y - 1 ) mod 5 ) >. =/= <. 0 , ( ( y - 1 ) mod 5 ) >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) )
100 96 99 biimtrdi 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) 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 >. ) ) ) )
101 100 impd 
 |-  ( ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) 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 >. ) ) )
102 101 ex 
 |-  ( L = <. 0 , ( ( y - 1 ) mod 5 ) >. -> ( K = <. 0 , ( ( y - 1 ) 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 >. ) ) ) )
103 87 93 102 3jaod 
 |-  ( 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
104 48 79 103 3jaoi 
 |-  ( ( 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
105 104 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) )
106 25 105 biimtrdi 
 |-  ( ( X = <. 0 , y >. /\ X e. V ) -> ( ( ( 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
107 106 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 = <. 0 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) ) )