Metamath Proof Explorer

Theorem pgnbgreunbgrlem3

Description: Lemma 3 for pgnbgreunbgr . (Contributed by AV, 18-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 pgnbgreunbgrlem3 
|- ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b 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 2 nbgrcl 
 |-  ( K e. ( G NeighbVtx X ) -> X e. V )
6 5 4 eleq2s 
 |-  ( K e. N -> X e. V )
7 6 3ad2ant1 
 |-  ( ( K e. N /\ L e. N /\ K =/= L ) -> X e. V )
8 5eluz3 
 |-  5 e. ( ZZ>= ` 3 )
9 pglem 
 |-  2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
10 eqid 
 |-  ( 0 ..^ 5 ) = ( 0 ..^ 5 )
11 eqid 
 |-  ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) = ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
12 10 11 1 2 gpgvtxel 
 |-  ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( X e. V <-> E. x e. { 0 , 1 } E. y e. ( 0 ..^ 5 ) X = <. x , y >. ) )
13 8 9 12 mp2an 
 |-  ( X e. V <-> E. x e. { 0 , 1 } E. y e. ( 0 ..^ 5 ) X = <. x , y >. )
14 13 biimpi 
 |-  ( X e. V -> E. x e. { 0 , 1 } E. y e. ( 0 ..^ 5 ) X = <. x , y >. )
15 14 adantl 
 |-  ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) -> E. x e. { 0 , 1 } E. y e. ( 0 ..^ 5 ) X = <. x , y >. )
16 vex 
 |-  x e. _V
17 16 elpr 
 |-  ( x e. { 0 , 1 } <-> ( x = 0 \/ x = 1 ) )
18 opeq1 
 |-  ( x = 0 -> <. x , y >. = <. 0 , y >. )
19 18 eqeq2d 
 |-  ( x = 0 -> ( X = <. x , y >. <-> X = <. 0 , y >. ) )
20 19 adantr 
 |-  ( ( x = 0 /\ ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( X = <. x , y >. <-> X = <. 0 , y >. ) )
21 8 9 pm3.2i 
 |-  ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) )
22 2 eleq2i 
 |-  ( X e. V <-> X e. ( Vtx ` G ) )
23 22 biimpi 
 |-  ( X e. V -> X e. ( Vtx ` G ) )
24 c0ex 
 |-  0 e. _V
25 vex 
 |-  y e. _V
26 24 25 op1std 
 |-  ( X = <. 0 , y >. -> ( 1st ` X ) = 0 )
27 23 26 anim12i 
 |-  ( ( X e. V /\ X = <. 0 , y >. ) -> ( X e. ( Vtx ` G ) /\ ( 1st ` X ) = 0 ) )
28 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
29 11 1 28 4 gpgnbgrvtx0 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ ( X e. ( Vtx ` G ) /\ ( 1st ` X ) = 0 ) ) -> N = { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } )
30 21 27 29 sylancr 
 |-  ( ( X e. V /\ X = <. 0 , y >. ) -> N = { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } )
31 eleq2 
 |-  ( N = { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } -> ( K e. N <-> K e. { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } ) )
32 eleq2 
 |-  ( N = { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } -> ( L e. N <-> L e. { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } ) )
33 31 32 anbi12d 
 |-  ( N = { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } -> ( ( K e. N /\ L e. N ) <-> ( K e. { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } /\ L e. { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } ) ) )
34 33 adantl 
 |-  ( ( ( X e. V /\ X = <. 0 , y >. ) /\ N = { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } ) -> ( ( K e. N /\ L e. N ) <-> ( K e. { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } /\ L e. { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } ) ) )
35 eltpi 
 |-  ( K e. { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } -> ( K = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ K = <. 1 , ( 2nd ` X ) >. \/ K = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) )
36 eltpi 
 |-  ( L e. { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } -> ( L = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. \/ L = <. 1 , ( 2nd ` X ) >. \/ L = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. ) )
37 1 2 3 4 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 >. ) ) ) ) )
38 36 37 syl 
 |-  ( L e. { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 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 >. ) ) ) ) )
39 35 38 mpan9 
 |-  ( ( K e. { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } /\ L e. { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 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 >. ) ) ) )
40 39 com12 
 |-  ( ( X e. V /\ X = <. 0 , y >. ) -> ( ( K e. { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } /\ L e. { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 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 >. ) ) ) )
41 40 adantr 
 |-  ( ( ( X e. V /\ X = <. 0 , y >. ) /\ N = { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } ) -> ( ( K e. { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } /\ L e. { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 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 >. ) ) ) )
42 34 41 sylbid 
 |-  ( ( ( X e. V /\ X = <. 0 , y >. ) /\ N = { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } ) -> ( ( K e. N /\ L e. N ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
43 30 42 mpdan 
 |-  ( ( X e. V /\ X = <. 0 , y >. ) -> ( ( K e. N /\ L e. N ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
44 43 com12 
 |-  ( ( K e. N /\ L e. N ) -> ( ( 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 >. ) ) ) )
45 44 expd 
 |-  ( ( K e. N /\ L e. N ) -> ( 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 >. ) ) ) ) )
46 45 com23 
 |-  ( ( K e. N /\ L e. N ) -> ( X = <. 0 , y >. -> ( X e. V -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
47 46 com24 
 |-  ( ( K e. N /\ L e. N ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( X e. V -> ( X = <. 0 , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
48 47 expd 
 |-  ( ( K e. N /\ L e. N ) -> ( K =/= L -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( X e. V -> ( X = <. 0 , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) ) )
49 48 3impia 
 |-  ( ( K e. N /\ L e. N /\ K =/= L ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( X e. V -> ( X = <. 0 , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
50 49 expdimp 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) -> ( y e. ( 0 ..^ 5 ) -> ( X e. V -> ( X = <. 0 , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
51 50 com23 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) -> ( X e. V -> ( y e. ( 0 ..^ 5 ) -> ( X = <. 0 , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
52 51 imp31 
 |-  ( ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) /\ y e. ( 0 ..^ 5 ) ) -> ( X = <. 0 , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
53 52 adantl 
 |-  ( ( x = 0 /\ ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( X = <. 0 , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
54 20 53 sylbid 
 |-  ( ( x = 0 /\ ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( X = <. x , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
55 54 ex 
 |-  ( x = 0 -> ( ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) /\ y e. ( 0 ..^ 5 ) ) -> ( X = <. x , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
56 1ex 
 |-  1 e. _V
57 56 25 op1std 
 |-  ( X = <. 1 , y >. -> ( 1st ` X ) = 1 )
58 57 anim1ci 
 |-  ( ( X = <. 1 , y >. /\ X e. V ) -> ( X e. V /\ ( 1st ` X ) = 1 ) )
59 11 1 2 4 gpgnbgrvtx1 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> N = { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } )
60 21 58 59 sylancr 
 |-  ( ( X = <. 1 , y >. /\ X e. V ) -> N = { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } )
61 eleq2 
 |-  ( N = { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } -> ( K e. N <-> K e. { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } ) )
62 eleq2 
 |-  ( N = { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } -> ( L e. N <-> L e. { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } ) )
63 61 62 anbi12d 
 |-  ( N = { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } -> ( ( K e. N /\ L e. N ) <-> ( K e. { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } /\ L e. { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } ) ) )
64 63 adantl 
 |-  ( ( ( X = <. 1 , y >. /\ X e. V ) /\ N = { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } ) -> ( ( K e. N /\ L e. N ) <-> ( K e. { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } /\ L e. { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } ) ) )
65 eltpi 
 |-  ( K e. { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } -> ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ K = <. 0 , ( 2nd ` X ) >. \/ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) )
66 eltpi 
 |-  ( L e. { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } -> ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ L = <. 0 , ( 2nd ` X ) >. \/ L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) )
67 1 2 3 4 pgnbgreunbgrlem2 
 |-  ( ( 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 = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
68 66 67 syl 
 |-  ( L e. { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 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 = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
69 65 68 mpan9 
 |-  ( ( K e. { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } /\ L e. { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } ) -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
70 69 com12 
 |-  ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K e. { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } /\ L e. { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) 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 >. ) ) ) )
71 70 adantr 
 |-  ( ( ( X = <. 1 , y >. /\ X e. V ) /\ N = { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } ) -> ( ( K e. { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } /\ L e. { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) 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 >. ) ) ) )
72 64 71 sylbid 
 |-  ( ( ( X = <. 1 , y >. /\ X e. V ) /\ N = { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } ) -> ( ( K e. N /\ L e. N ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
73 60 72 mpdan 
 |-  ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K e. N /\ L e. N ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
74 73 com12 
 |-  ( ( K e. N /\ L e. N ) -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
75 74 expd 
 |-  ( ( K e. N /\ L e. N ) -> ( X = <. 1 , y >. -> ( X e. V -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
76 75 com24 
 |-  ( ( K e. N /\ L e. N ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( X e. V -> ( X = <. 1 , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
77 76 expd 
 |-  ( ( K e. N /\ L e. N ) -> ( K =/= L -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( X e. V -> ( X = <. 1 , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) ) )
78 77 3impia 
 |-  ( ( K e. N /\ L e. N /\ K =/= L ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( X e. V -> ( X = <. 1 , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
79 78 expdimp 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) -> ( y e. ( 0 ..^ 5 ) -> ( X e. V -> ( X = <. 1 , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
80 79 com23 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) -> ( X e. V -> ( y e. ( 0 ..^ 5 ) -> ( X = <. 1 , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
81 80 imp31 
 |-  ( ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) /\ y e. ( 0 ..^ 5 ) ) -> ( X = <. 1 , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
82 opeq1 
 |-  ( x = 1 -> <. x , y >. = <. 1 , y >. )
83 82 eqeq2d 
 |-  ( x = 1 -> ( X = <. x , y >. <-> X = <. 1 , y >. ) )
84 83 imbi1d 
 |-  ( x = 1 -> ( ( X = <. x , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) <-> ( X = <. 1 , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
85 81 84 imbitrrid 
 |-  ( x = 1 -> ( ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) /\ y e. ( 0 ..^ 5 ) ) -> ( X = <. x , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
86 55 85 jaoi 
 |-  ( ( x = 0 \/ x = 1 ) -> ( ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) /\ y e. ( 0 ..^ 5 ) ) -> ( X = <. x , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
87 17 86 sylbi 
 |-  ( x e. { 0 , 1 } -> ( ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) /\ y e. ( 0 ..^ 5 ) ) -> ( X = <. x , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
88 87 expd 
 |-  ( x e. { 0 , 1 } -> ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) -> ( y e. ( 0 ..^ 5 ) -> ( X = <. x , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
89 88 com12 
 |-  ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) -> ( x e. { 0 , 1 } -> ( y e. ( 0 ..^ 5 ) -> ( X = <. x , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
90 89 impd 
 |-  ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) -> ( ( x e. { 0 , 1 } /\ y e. ( 0 ..^ 5 ) ) -> ( X = <. x , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
91 90 rexlimdvv 
 |-  ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) -> ( E. x e. { 0 , 1 } E. y e. ( 0 ..^ 5 ) X = <. x , y >. -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
92 15 91 mpd 
 |-  ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) )
93 7 92 mpidan 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) )