Metamath Proof Explorer

Theorem pgnbgreunbgrlem6

Description: Lemma 6 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 pgnbgreunbgrlem6 
|- ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b 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 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 8 9 pm3.2i 
 |-  ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) )
19 c0ex 
 |-  0 e. _V
20 vex 
 |-  y e. _V
21 19 20 op1std 
 |-  ( X = <. 0 , y >. -> ( 1st ` X ) = 0 )
22 21 anim1ci 
 |-  ( ( X = <. 0 , y >. /\ X e. V ) -> ( X e. V /\ ( 1st ` X ) = 0 ) )
23 11 1 2 4 gpgnbgrvtx0 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> N = { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } )
24 18 22 23 sylancr 
 |-  ( ( X = <. 0 , y >. /\ X e. V ) -> N = { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod 5 ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod 5 ) >. } )
25 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 ) >. } ) )
26 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 ) >. } ) )
27 25 26 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 ) >. } ) ) )
28 27 adantl 
 |-  ( ( ( X = <. 0 , y >. /\ X e. V ) /\ 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 ) >. } ) ) )
29 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 ) >. ) )
30 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 ) >. ) )
31 1 2 3 4 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 >. ) ) ) ) )
32 30 31 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 = <. 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 >. ) ) ) ) )
33 29 32 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 = <. 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 >. ) ) ) )
34 33 com12 
 |-  ( ( X = <. 0 , y >. /\ X e. V ) -> ( ( 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
35 34 adantr 
 |-  ( ( ( X = <. 0 , y >. /\ X e. V ) /\ 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
36 28 35 sylbid 
 |-  ( ( ( X = <. 0 , y >. /\ X e. V ) /\ 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
37 24 36 mpdan 
 |-  ( ( X = <. 0 , y >. /\ X e. V ) -> ( ( K e. N /\ L e. N ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
38 37 com12 
 |-  ( ( K e. N /\ L e. N ) -> ( ( 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 >. ) ) ) )
39 38 expd 
 |-  ( ( K e. N /\ L e. N ) -> ( 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 >. ) ) ) ) )
40 39 com24 
 |-  ( ( K e. N /\ L e. N ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( X e. V -> ( X = <. 0 , y >. -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) ) )
41 40 expd 
 |-  ( ( K e. N /\ L e. N ) -> ( K =/= L -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( X e. V -> ( X = <. 0 , y >. -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) ) ) )
42 41 3impia 
 |-  ( ( K e. N /\ L e. N /\ K =/= L ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( X e. V -> ( X = <. 0 , y >. -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) ) )
43 42 expdimp 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) -> ( y e. ( 0 ..^ 5 ) -> ( X e. V -> ( X = <. 0 , y >. -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) ) )
44 43 com23 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) -> ( X e. V -> ( y e. ( 0 ..^ 5 ) -> ( X = <. 0 , y >. -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) ) )
45 44 imp31 
 |-  ( ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) /\ y e. ( 0 ..^ 5 ) ) -> ( X = <. 0 , y >. -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) )
46 opeq1 
 |-  ( x = 0 -> <. x , y >. = <. 0 , y >. )
47 46 eqeq2d 
 |-  ( x = 0 -> ( X = <. x , y >. <-> X = <. 0 , y >. ) )
48 47 imbi1d 
 |-  ( x = 0 -> ( ( X = <. x , y >. -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) <-> ( X = <. 0 , y >. -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
49 45 48 imbitrrid 
 |-  ( 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
50 opeq1 
 |-  ( x = 1 -> <. x , y >. = <. 1 , y >. )
51 50 eqeq2d 
 |-  ( x = 1 -> ( X = <. x , y >. <-> X = <. 1 , y >. ) )
52 51 adantr 
 |-  ( ( x = 1 /\ ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( X = <. x , y >. <-> X = <. 1 , y >. ) )
53 2 eleq2i 
 |-  ( X e. V <-> X e. ( Vtx ` G ) )
54 53 biimpi 
 |-  ( X e. V -> X e. ( Vtx ` G ) )
55 1ex 
 |-  1 e. _V
56 55 20 op1std 
 |-  ( X = <. 1 , y >. -> ( 1st ` X ) = 1 )
57 54 56 anim12i 
 |-  ( ( X e. V /\ X = <. 1 , y >. ) -> ( X e. ( Vtx ` G ) /\ ( 1st ` X ) = 1 ) )
58 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
59 11 1 58 4 gpgnbgrvtx1 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ ( X e. ( Vtx ` G ) /\ ( 1st ` X ) = 1 ) ) -> N = { <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. } )
60 18 57 59 sylancr 
 |-  ( ( X e. V /\ X = <. 1 , y >. ) -> 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 e. V /\ X = <. 1 , y >. ) /\ 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 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 >. ) ) ) ) )
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 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 >. ) ) ) ) )
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 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 >. ) ) ) )
70 69 com12 
 |-  ( ( X e. V /\ X = <. 1 , y >. ) -> ( ( 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
71 70 adantr 
 |-  ( ( ( X e. V /\ X = <. 1 , y >. ) /\ 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
72 64 71 sylbid 
 |-  ( ( ( X e. V /\ X = <. 1 , y >. ) /\ 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
73 60 72 mpdan 
 |-  ( ( X e. V /\ X = <. 1 , y >. ) -> ( ( K e. N /\ L e. N ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
74 73 com12 
 |-  ( ( K e. N /\ L e. N ) -> ( ( 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 >. ) ) ) )
75 74 expd 
 |-  ( ( K e. N /\ L e. N ) -> ( 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 >. ) ) ) ) )
76 75 com23 
 |-  ( ( K e. N /\ L e. N ) -> ( X = <. 1 , 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 >. ) ) ) ) )
77 76 com24 
 |-  ( ( K e. N /\ L e. N ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( X e. V -> ( X = <. 1 , y >. -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) ) )
78 77 expd 
 |-  ( ( K e. N /\ L e. N ) -> ( K =/= L -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( X e. V -> ( X = <. 1 , y >. -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) ) ) )
79 78 3impia 
 |-  ( ( K e. N /\ L e. N /\ K =/= L ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( X e. V -> ( X = <. 1 , y >. -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) ) )
80 79 expdimp 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) -> ( y e. ( 0 ..^ 5 ) -> ( X e. V -> ( X = <. 1 , y >. -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) ) )
81 80 com23 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) -> ( X e. V -> ( y e. ( 0 ..^ 5 ) -> ( X = <. 1 , y >. -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) ) )
82 81 imp31 
 |-  ( ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) /\ y e. ( 0 ..^ 5 ) ) -> ( X = <. 1 , y >. -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) )
83 82 adantl 
 |-  ( ( x = 1 /\ ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( X = <. 1 , y >. -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) )
84 52 83 sylbid 
 |-  ( ( 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) )
85 84 ex 
 |-  ( 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) ) )
86 49 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , 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 , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) )
92 15 91 mpd 
 |-  ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) /\ X e. V ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) )
93 7 92 mpidan 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) )