Metamath Proof Explorer

Theorem gpgprismgr4cycllem10

Description: Lemma 10 for gpgprismgr4cycl0 . (Contributed by AV, 5-Nov-2025)

Ref Expression
Hypotheses gpgprismgr4cycl.p 
|- P = <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. ">
gpgprismgr4cycl.f 
|- F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } ">
gpgprismgr4cycl.g 
|- G = ( N gPetersenGr 1 )
Assertion gpgprismgr4cycllem10 
|- ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` G ) ` ( F ` X ) ) = { ( P ` X ) , ( P ` ( X + 1 ) ) } )

Proof

Step Hyp Ref Expression
1 gpgprismgr4cycl.p 
 |-  P = <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. ">
2 gpgprismgr4cycl.f 
 |-  F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } ">
3 gpgprismgr4cycl.g 
 |-  G = ( N gPetersenGr 1 )
4 3 fveq2i 
 |-  ( iEdg ` G ) = ( iEdg ` ( N gPetersenGr 1 ) )
5 4 a1i 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( iEdg ` G ) = ( iEdg ` ( N gPetersenGr 1 ) ) )
6 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
7 1elfzo1ceilhalf1 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
8 6 7 jca 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N e. NN /\ 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) )
9 8 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( N e. NN /\ 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) )
10 eqid 
 |-  ( 1 ..^ ( |^ ` ( N / 2 ) ) ) = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
11 eqid 
 |-  ( 0 ..^ N ) = ( 0 ..^ N )
12 10 11 gpgiedg 
 |-  ( ( N e. NN /\ 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( iEdg ` ( N gPetersenGr 1 ) ) = ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) } ) )
13 9 12 syl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( iEdg ` ( N gPetersenGr 1 ) ) = ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) } ) )
14 5 13 eqtrd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( iEdg ` G ) = ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) } ) )
15 14 fveq1d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` G ) ` ( F ` X ) ) = ( ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) } ) ` ( F ` X ) ) )
16 2 gpgprismgr4cycllem3 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ 4 ) ) -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
17 2 gpgprismgr4cycllem1 
 |-  ( # ` F ) = 4
18 17 oveq2i 
 |-  ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 )
19 18 eleq2i 
 |-  ( X e. ( 0 ..^ ( # ` F ) ) <-> X e. ( 0 ..^ 4 ) )
20 19 anbi2i 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ ( # ` F ) ) ) <-> ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ 4 ) ) )
21 eqeq1 
 |-  ( e = ( F ` X ) -> ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) )
22 eqeq1 
 |-  ( e = ( F ` X ) -> ( e = { <. 0 , x >. , <. 1 , x >. } <-> ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } ) )
23 eqeq1 
 |-  ( e = ( F ` X ) -> ( e = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
24 21 22 23 3orbi123d 
 |-  ( e = ( F ` X ) -> ( ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
25 24 rexbidv 
 |-  ( e = ( F ` X ) -> ( E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
26 25 elrab 
 |-  ( ( F ` X ) e. { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) } <-> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
27 16 20 26 3imtr4i 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` X ) e. { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) } )
28 fvresi 
 |-  ( ( F ` X ) e. { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) } -> ( ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) } ) ` ( F ` X ) ) = ( F ` X ) )
29 27 28 syl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) } ) ` ( F ` X ) ) = ( F ` X ) )
30 15 29 eqtrd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` G ) ` ( F ` X ) ) = ( F ` X ) )
31 fzo0to42pr 
 |-  ( 0 ..^ 4 ) = ( { 0 , 1 } u. { 2 , 3 } )
32 31 eleq2i 
 |-  ( X e. ( 0 ..^ 4 ) <-> X e. ( { 0 , 1 } u. { 2 , 3 } ) )
33 elun 
 |-  ( X e. ( { 0 , 1 } u. { 2 , 3 } ) <-> ( X e. { 0 , 1 } \/ X e. { 2 , 3 } ) )
34 19 32 33 3bitri 
 |-  ( X e. ( 0 ..^ ( # ` F ) ) <-> ( X e. { 0 , 1 } \/ X e. { 2 , 3 } ) )
35 elpri 
 |-  ( X e. { 0 , 1 } -> ( X = 0 \/ X = 1 ) )
36 prex 
 |-  { <. 0 , 0 >. , <. 0 , 1 >. } e. _V
37 s4fv0 
 |-  ( { <. 0 , 0 >. , <. 0 , 1 >. } e. _V -> ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 0 ) = { <. 0 , 0 >. , <. 0 , 1 >. } )
38 36 37 ax-mp 
 |-  ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 0 ) = { <. 0 , 0 >. , <. 0 , 1 >. }
39 2 fveq1i 
 |-  ( F ` 0 ) = ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 0 )
40 1 fveq1i 
 |-  ( P ` 0 ) = ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 0 )
41 opex 
 |-  <. 0 , 0 >. e. _V
42 df-s5 
 |-  <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> = ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. "> ++ <" <. 0 , 0 >. "> )
43 s4cli 
 |-  <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. "> e. Word _V
44 s4len 
 |-  ( # ` <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. "> ) = 4
45 s4fv0 
 |-  ( <. 0 , 0 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. "> ` 0 ) = <. 0 , 0 >. )
46 0nn0 
 |-  0 e. NN0
47 4pos 
 |-  0 < 4
48 42 43 44 45 46 47 cats1fv 
 |-  ( <. 0 , 0 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 0 ) = <. 0 , 0 >. )
49 41 48 ax-mp 
 |-  ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 0 ) = <. 0 , 0 >.
50 40 49 eqtri 
 |-  ( P ` 0 ) = <. 0 , 0 >.
51 1 fveq1i 
 |-  ( P ` 1 ) = ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 1 )
52 opex 
 |-  <. 0 , 1 >. e. _V
53 s4fv1 
 |-  ( <. 0 , 1 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. "> ` 1 ) = <. 0 , 1 >. )
54 1nn0 
 |-  1 e. NN0
55 1lt4 
 |-  1 < 4
56 42 43 44 53 54 55 cats1fv 
 |-  ( <. 0 , 1 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 1 ) = <. 0 , 1 >. )
57 52 56 ax-mp 
 |-  ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 1 ) = <. 0 , 1 >.
58 51 57 eqtri 
 |-  ( P ` 1 ) = <. 0 , 1 >.
59 50 58 preq12i 
 |-  { ( P ` 0 ) , ( P ` 1 ) } = { <. 0 , 0 >. , <. 0 , 1 >. }
60 38 39 59 3eqtr4i 
 |-  ( F ` 0 ) = { ( P ` 0 ) , ( P ` 1 ) }
61 fveq2 
 |-  ( X = 0 -> ( F ` X ) = ( F ` 0 ) )
62 fveq2 
 |-  ( X = 0 -> ( P ` X ) = ( P ` 0 ) )
63 fv0p1e1 
 |-  ( X = 0 -> ( P ` ( X + 1 ) ) = ( P ` 1 ) )
64 62 63 preq12d 
 |-  ( X = 0 -> { ( P ` X ) , ( P ` ( X + 1 ) ) } = { ( P ` 0 ) , ( P ` 1 ) } )
65 60 61 64 3eqtr4a 
 |-  ( X = 0 -> ( F ` X ) = { ( P ` X ) , ( P ` ( X + 1 ) ) } )
66 prex 
 |-  { <. 0 , 1 >. , <. 1 , 1 >. } e. _V
67 s4fv1 
 |-  ( { <. 0 , 1 >. , <. 1 , 1 >. } e. _V -> ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 1 ) = { <. 0 , 1 >. , <. 1 , 1 >. } )
68 66 67 ax-mp 
 |-  ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 1 ) = { <. 0 , 1 >. , <. 1 , 1 >. }
69 2 fveq1i 
 |-  ( F ` 1 ) = ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 1 )
70 1 fveq1i 
 |-  ( P ` 2 ) = ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 2 )
71 opex 
 |-  <. 1 , 1 >. e. _V
72 s4fv2 
 |-  ( <. 1 , 1 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. "> ` 2 ) = <. 1 , 1 >. )
73 2nn0 
 |-  2 e. NN0
74 2lt4 
 |-  2 < 4
75 42 43 44 72 73 74 cats1fv 
 |-  ( <. 1 , 1 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 2 ) = <. 1 , 1 >. )
76 71 75 ax-mp 
 |-  ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 2 ) = <. 1 , 1 >.
77 70 76 eqtri 
 |-  ( P ` 2 ) = <. 1 , 1 >.
78 58 77 preq12i 
 |-  { ( P ` 1 ) , ( P ` 2 ) } = { <. 0 , 1 >. , <. 1 , 1 >. }
79 68 69 78 3eqtr4i 
 |-  ( F ` 1 ) = { ( P ` 1 ) , ( P ` 2 ) }
80 fveq2 
 |-  ( X = 1 -> ( F ` X ) = ( F ` 1 ) )
81 fveq2 
 |-  ( X = 1 -> ( P ` X ) = ( P ` 1 ) )
82 oveq1 
 |-  ( X = 1 -> ( X + 1 ) = ( 1 + 1 ) )
83 1p1e2 
 |-  ( 1 + 1 ) = 2
84 82 83 eqtrdi 
 |-  ( X = 1 -> ( X + 1 ) = 2 )
85 84 fveq2d 
 |-  ( X = 1 -> ( P ` ( X + 1 ) ) = ( P ` 2 ) )
86 81 85 preq12d 
 |-  ( X = 1 -> { ( P ` X ) , ( P ` ( X + 1 ) ) } = { ( P ` 1 ) , ( P ` 2 ) } )
87 79 80 86 3eqtr4a 
 |-  ( X = 1 -> ( F ` X ) = { ( P ` X ) , ( P ` ( X + 1 ) ) } )
88 65 87 jaoi 
 |-  ( ( X = 0 \/ X = 1 ) -> ( F ` X ) = { ( P ` X ) , ( P ` ( X + 1 ) ) } )
89 35 88 syl 
 |-  ( X e. { 0 , 1 } -> ( F ` X ) = { ( P ` X ) , ( P ` ( X + 1 ) ) } )
90 elpri 
 |-  ( X e. { 2 , 3 } -> ( X = 2 \/ X = 3 ) )
91 prex 
 |-  { <. 1 , 1 >. , <. 1 , 0 >. } e. _V
92 s4fv2 
 |-  ( { <. 1 , 1 >. , <. 1 , 0 >. } e. _V -> ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 2 ) = { <. 1 , 1 >. , <. 1 , 0 >. } )
93 91 92 ax-mp 
 |-  ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 2 ) = { <. 1 , 1 >. , <. 1 , 0 >. }
94 2 fveq1i 
 |-  ( F ` 2 ) = ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 2 )
95 1 fveq1i 
 |-  ( P ` 3 ) = ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 3 )
96 opex 
 |-  <. 1 , 0 >. e. _V
97 s4fv3 
 |-  ( <. 1 , 0 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. "> ` 3 ) = <. 1 , 0 >. )
98 3nn0 
 |-  3 e. NN0
99 3lt4 
 |-  3 < 4
100 42 43 44 97 98 99 cats1fv 
 |-  ( <. 1 , 0 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 3 ) = <. 1 , 0 >. )
101 96 100 ax-mp 
 |-  ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 3 ) = <. 1 , 0 >.
102 95 101 eqtri 
 |-  ( P ` 3 ) = <. 1 , 0 >.
103 77 102 preq12i 
 |-  { ( P ` 2 ) , ( P ` 3 ) } = { <. 1 , 1 >. , <. 1 , 0 >. }
104 93 94 103 3eqtr4i 
 |-  ( F ` 2 ) = { ( P ` 2 ) , ( P ` 3 ) }
105 fveq2 
 |-  ( X = 2 -> ( F ` X ) = ( F ` 2 ) )
106 fveq2 
 |-  ( X = 2 -> ( P ` X ) = ( P ` 2 ) )
107 oveq1 
 |-  ( X = 2 -> ( X + 1 ) = ( 2 + 1 ) )
108 2p1e3 
 |-  ( 2 + 1 ) = 3
109 107 108 eqtrdi 
 |-  ( X = 2 -> ( X + 1 ) = 3 )
110 109 fveq2d 
 |-  ( X = 2 -> ( P ` ( X + 1 ) ) = ( P ` 3 ) )
111 106 110 preq12d 
 |-  ( X = 2 -> { ( P ` X ) , ( P ` ( X + 1 ) ) } = { ( P ` 2 ) , ( P ` 3 ) } )
112 104 105 111 3eqtr4a 
 |-  ( X = 2 -> ( F ` X ) = { ( P ` X ) , ( P ` ( X + 1 ) ) } )
113 prex 
 |-  { <. 1 , 0 >. , <. 0 , 0 >. } e. _V
114 s4fv3 
 |-  ( { <. 1 , 0 >. , <. 0 , 0 >. } e. _V -> ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 3 ) = { <. 1 , 0 >. , <. 0 , 0 >. } )
115 113 114 ax-mp 
 |-  ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 3 ) = { <. 1 , 0 >. , <. 0 , 0 >. }
116 2 fveq1i 
 |-  ( F ` 3 ) = ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 3 )
117 1 fveq1i 
 |-  ( P ` 4 ) = ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 4 )
118 42 43 44 cats1fvn 
 |-  ( <. 0 , 0 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 4 ) = <. 0 , 0 >. )
119 41 118 ax-mp 
 |-  ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 4 ) = <. 0 , 0 >.
120 117 119 eqtri 
 |-  ( P ` 4 ) = <. 0 , 0 >.
121 102 120 preq12i 
 |-  { ( P ` 3 ) , ( P ` 4 ) } = { <. 1 , 0 >. , <. 0 , 0 >. }
122 115 116 121 3eqtr4i 
 |-  ( F ` 3 ) = { ( P ` 3 ) , ( P ` 4 ) }
123 fveq2 
 |-  ( X = 3 -> ( F ` X ) = ( F ` 3 ) )
124 fveq2 
 |-  ( X = 3 -> ( P ` X ) = ( P ` 3 ) )
125 oveq1 
 |-  ( X = 3 -> ( X + 1 ) = ( 3 + 1 ) )
126 3p1e4 
 |-  ( 3 + 1 ) = 4
127 125 126 eqtrdi 
 |-  ( X = 3 -> ( X + 1 ) = 4 )
128 127 fveq2d 
 |-  ( X = 3 -> ( P ` ( X + 1 ) ) = ( P ` 4 ) )
129 124 128 preq12d 
 |-  ( X = 3 -> { ( P ` X ) , ( P ` ( X + 1 ) ) } = { ( P ` 3 ) , ( P ` 4 ) } )
130 122 123 129 3eqtr4a 
 |-  ( X = 3 -> ( F ` X ) = { ( P ` X ) , ( P ` ( X + 1 ) ) } )
131 112 130 jaoi 
 |-  ( ( X = 2 \/ X = 3 ) -> ( F ` X ) = { ( P ` X ) , ( P ` ( X + 1 ) ) } )
132 90 131 syl 
 |-  ( X e. { 2 , 3 } -> ( F ` X ) = { ( P ` X ) , ( P ` ( X + 1 ) ) } )
133 89 132 jaoi 
 |-  ( ( X e. { 0 , 1 } \/ X e. { 2 , 3 } ) -> ( F ` X ) = { ( P ` X ) , ( P ` ( X + 1 ) ) } )
134 34 133 sylbi 
 |-  ( X e. ( 0 ..^ ( # ` F ) ) -> ( F ` X ) = { ( P ` X ) , ( P ` ( X + 1 ) ) } )
135 134 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` X ) = { ( P ` X ) , ( P ` ( X + 1 ) ) } )
136 30 135 eqtrd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` G ) ` ( F ` X ) ) = { ( P ` X ) , ( P ` ( X + 1 ) ) } )