Metamath Proof Explorer

Theorem gpgprismgr4cycllem3

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

Ref Expression
Hypothesis gpgprismgr4cycllem1.f 
|- F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } ">
Assertion 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 ) >. } ) ) )

Proof

Step Hyp Ref Expression
1 gpgprismgr4cycllem1.f 
 |-  F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } ">
2 fzo0to42pr 
 |-  ( 0 ..^ 4 ) = ( { 0 , 1 } u. { 2 , 3 } )
3 2 eleq2i 
 |-  ( X e. ( 0 ..^ 4 ) <-> X e. ( { 0 , 1 } u. { 2 , 3 } ) )
4 elun 
 |-  ( X e. ( { 0 , 1 } u. { 2 , 3 } ) <-> ( X e. { 0 , 1 } \/ X e. { 2 , 3 } ) )
5 3 4 bitri 
 |-  ( X e. ( 0 ..^ 4 ) <-> ( X e. { 0 , 1 } \/ X e. { 2 , 3 } ) )
6 elpri 
 |-  ( X e. { 0 , 1 } -> ( X = 0 \/ X = 1 ) )
7 c0ex 
 |-  0 e. _V
8 7 prid1 
 |-  0 e. { 0 , 1 }
9 8 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> 0 e. { 0 , 1 } )
10 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
11 lbfzo0 
 |-  ( 0 e. ( 0 ..^ N ) <-> N e. NN )
12 10 11 sylibr 
 |-  ( N e. ( ZZ>= ` 3 ) -> 0 e. ( 0 ..^ N ) )
13 9 12 opelxpd 
 |-  ( N e. ( ZZ>= ` 3 ) -> <. 0 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
14 1nn0 
 |-  1 e. NN0
15 14 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. NN0 )
16 uzuzle23 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
17 eluz2gt1 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 < N )
18 16 17 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 < N )
19 elfzo0 
 |-  ( 1 e. ( 0 ..^ N ) <-> ( 1 e. NN0 /\ N e. NN /\ 1 < N ) )
20 15 10 18 19 syl3anbrc 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. ( 0 ..^ N ) )
21 9 20 opelxpd 
 |-  ( N e. ( ZZ>= ` 3 ) -> <. 0 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
22 prelpwi 
 |-  ( ( <. 0 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 0 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) )
23 13 21 22 syl2anc 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) )
24 opeq2 
 |-  ( x = 0 -> <. 0 , x >. = <. 0 , 0 >. )
25 oveq1 
 |-  ( x = 0 -> ( x + 1 ) = ( 0 + 1 ) )
26 25 oveq1d 
 |-  ( x = 0 -> ( ( x + 1 ) mod N ) = ( ( 0 + 1 ) mod N ) )
27 26 opeq2d 
 |-  ( x = 0 -> <. 0 , ( ( x + 1 ) mod N ) >. = <. 0 , ( ( 0 + 1 ) mod N ) >. )
28 24 27 preq12d 
 |-  ( x = 0 -> { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } )
29 28 eqeq2d 
 |-  ( x = 0 -> ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } ) )
30 opeq2 
 |-  ( x = 0 -> <. 1 , x >. = <. 1 , 0 >. )
31 24 30 preq12d 
 |-  ( x = 0 -> { <. 0 , x >. , <. 1 , x >. } = { <. 0 , 0 >. , <. 1 , 0 >. } )
32 31 eqeq2d 
 |-  ( x = 0 -> ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } <-> { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } ) )
33 26 opeq2d 
 |-  ( x = 0 -> <. 1 , ( ( x + 1 ) mod N ) >. = <. 1 , ( ( 0 + 1 ) mod N ) >. )
34 30 33 preq12d 
 |-  ( x = 0 -> { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } )
35 34 eqeq2d 
 |-  ( x = 0 -> ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) )
36 29 32 35 3orbi123d 
 |-  ( x = 0 -> ( ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) ) )
37 eluzelre 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. RR )
38 1mod 
 |-  ( ( N e. RR /\ 1 < N ) -> ( 1 mod N ) = 1 )
39 37 18 38 syl2anc 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( 1 mod N ) = 1 )
40 1e0p1 
 |-  1 = ( 0 + 1 )
41 40 oveq1i 
 |-  ( 1 mod N ) = ( ( 0 + 1 ) mod N )
42 39 41 eqtr3di 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 = ( ( 0 + 1 ) mod N ) )
43 42 opeq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> <. 0 , 1 >. = <. 0 , ( ( 0 + 1 ) mod N ) >. )
44 43 preq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } )
45 44 3mix1d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) )
46 36 12 45 rspcedvdw 
 |-  ( N e. ( ZZ>= ` 3 ) -> E. x e. ( 0 ..^ N ) ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
47 23 46 jca 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 0 , 0 >. , <. 0 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
48 fveq2 
 |-  ( X = 0 -> ( F ` X ) = ( F ` 0 ) )
49 1 fveq1i 
 |-  ( F ` 0 ) = ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 0 )
50 prex 
 |-  { <. 0 , 0 >. , <. 0 , 1 >. } e. _V
51 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 >. } )
52 50 51 ax-mp 
 |-  ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 0 ) = { <. 0 , 0 >. , <. 0 , 1 >. }
53 49 52 eqtri 
 |-  ( F ` 0 ) = { <. 0 , 0 >. , <. 0 , 1 >. }
54 48 53 eqtrdi 
 |-  ( X = 0 -> ( F ` X ) = { <. 0 , 0 >. , <. 0 , 1 >. } )
55 54 eleq1d 
 |-  ( X = 0 -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) <-> { <. 0 , 0 >. , <. 0 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
56 54 eqeq1d 
 |-  ( X = 0 -> ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) )
57 54 eqeq1d 
 |-  ( X = 0 -> ( ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } <-> { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } ) )
58 54 eqeq1d 
 |-  ( X = 0 -> ( ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
59 56 57 58 3orbi123d 
 |-  ( X = 0 -> ( ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
60 59 rexbidv 
 |-  ( X = 0 -> ( 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 ) >. } ) <-> E. x e. ( 0 ..^ N ) ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
61 55 60 anbi12d 
 |-  ( X = 0 -> ( ( ( 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 ) >. } ) ) <-> ( { <. 0 , 0 >. , <. 0 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
62 47 61 imbitrrid 
 |-  ( X = 0 -> ( N e. ( ZZ>= ` 3 ) -> ( ( 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 ) >. } ) ) ) )
63 1ex 
 |-  1 e. _V
64 63 prid2 
 |-  1 e. { 0 , 1 }
65 64 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. { 0 , 1 } )
66 65 20 opelxpd 
 |-  ( N e. ( ZZ>= ` 3 ) -> <. 1 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
67 prelpwi 
 |-  ( ( <. 0 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 1 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) )
68 21 66 67 syl2anc 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) )
69 opeq2 
 |-  ( x = 1 -> <. 0 , x >. = <. 0 , 1 >. )
70 oveq1 
 |-  ( x = 1 -> ( x + 1 ) = ( 1 + 1 ) )
71 70 oveq1d 
 |-  ( x = 1 -> ( ( x + 1 ) mod N ) = ( ( 1 + 1 ) mod N ) )
72 71 opeq2d 
 |-  ( x = 1 -> <. 0 , ( ( x + 1 ) mod N ) >. = <. 0 , ( ( 1 + 1 ) mod N ) >. )
73 69 72 preq12d 
 |-  ( x = 1 -> { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } = { <. 0 , 1 >. , <. 0 , ( ( 1 + 1 ) mod N ) >. } )
74 73 eqeq2d 
 |-  ( x = 1 -> ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 0 , ( ( 1 + 1 ) mod N ) >. } ) )
75 opeq2 
 |-  ( x = 1 -> <. 1 , x >. = <. 1 , 1 >. )
76 69 75 preq12d 
 |-  ( x = 1 -> { <. 0 , x >. , <. 1 , x >. } = { <. 0 , 1 >. , <. 1 , 1 >. } )
77 76 eqeq2d 
 |-  ( x = 1 -> ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } <-> { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 1 , 1 >. } ) )
78 71 opeq2d 
 |-  ( x = 1 -> <. 1 , ( ( x + 1 ) mod N ) >. = <. 1 , ( ( 1 + 1 ) mod N ) >. )
79 75 78 preq12d 
 |-  ( x = 1 -> { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } = { <. 1 , 1 >. , <. 1 , ( ( 1 + 1 ) mod N ) >. } )
80 79 eqeq2d 
 |-  ( x = 1 -> ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , 1 >. , <. 1 , ( ( 1 + 1 ) mod N ) >. } ) )
81 74 77 80 3orbi123d 
 |-  ( x = 1 -> ( ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 0 , ( ( 1 + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 1 , 1 >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , 1 >. , <. 1 , ( ( 1 + 1 ) mod N ) >. } ) ) )
82 eqid 
 |-  { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 1 , 1 >. }
83 82 3mix2i 
 |-  ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 0 , ( ( 1 + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 1 , 1 >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , 1 >. , <. 1 , ( ( 1 + 1 ) mod N ) >. } )
84 83 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 0 , ( ( 1 + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 1 , 1 >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , 1 >. , <. 1 , ( ( 1 + 1 ) mod N ) >. } ) )
85 81 20 84 rspcedvdw 
 |-  ( N e. ( ZZ>= ` 3 ) -> E. x e. ( 0 ..^ N ) ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
86 68 85 jca 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 0 , 1 >. , <. 1 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
87 fveq2 
 |-  ( X = 1 -> ( F ` X ) = ( F ` 1 ) )
88 1 fveq1i 
 |-  ( F ` 1 ) = ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 1 )
89 prex 
 |-  { <. 0 , 1 >. , <. 1 , 1 >. } e. _V
90 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 >. } )
91 89 90 ax-mp 
 |-  ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 1 ) = { <. 0 , 1 >. , <. 1 , 1 >. }
92 88 91 eqtri 
 |-  ( F ` 1 ) = { <. 0 , 1 >. , <. 1 , 1 >. }
93 87 92 eqtrdi 
 |-  ( X = 1 -> ( F ` X ) = { <. 0 , 1 >. , <. 1 , 1 >. } )
94 93 eleq1d 
 |-  ( X = 1 -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) <-> { <. 0 , 1 >. , <. 1 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
95 93 eqeq1d 
 |-  ( X = 1 -> ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) )
96 93 eqeq1d 
 |-  ( X = 1 -> ( ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } <-> { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } ) )
97 93 eqeq1d 
 |-  ( X = 1 -> ( ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
98 95 96 97 3orbi123d 
 |-  ( X = 1 -> ( ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
99 98 rexbidv 
 |-  ( X = 1 -> ( 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 ) >. } ) <-> E. x e. ( 0 ..^ N ) ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
100 94 99 anbi12d 
 |-  ( X = 1 -> ( ( ( 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 ) >. } ) ) <-> ( { <. 0 , 1 >. , <. 1 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
101 86 100 imbitrrid 
 |-  ( X = 1 -> ( N e. ( ZZ>= ` 3 ) -> ( ( 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 ) >. } ) ) ) )
102 62 101 jaoi 
 |-  ( ( X = 0 \/ X = 1 ) -> ( N e. ( ZZ>= ` 3 ) -> ( ( 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 ) >. } ) ) ) )
103 6 102 syl 
 |-  ( X e. { 0 , 1 } -> ( N e. ( ZZ>= ` 3 ) -> ( ( 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 ) >. } ) ) ) )
104 elpri 
 |-  ( X e. { 2 , 3 } -> ( X = 2 \/ X = 3 ) )
105 65 12 opelxpd 
 |-  ( N e. ( ZZ>= ` 3 ) -> <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
106 66 105 jca 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( <. 1 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
107 106 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X = 2 ) -> ( <. 1 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
108 prelpwi 
 |-  ( ( <. 1 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) )
109 107 108 syl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X = 2 ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) )
110 28 eqeq2d 
 |-  ( x = 0 -> ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } ) )
111 31 eqeq2d 
 |-  ( x = 0 -> ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } <-> { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } ) )
112 34 eqeq2d 
 |-  ( x = 0 -> ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) )
113 110 111 112 3orbi123d 
 |-  ( x = 0 -> ( ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) ) )
114 prcom 
 |-  { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , 0 >. , <. 1 , 1 >. }
115 42 opeq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> <. 1 , 1 >. = <. 1 , ( ( 0 + 1 ) mod N ) >. )
116 115 preq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } )
117 114 116 eqtrid 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } )
118 117 3mix3d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) )
119 113 12 118 rspcedvdw 
 |-  ( N e. ( ZZ>= ` 3 ) -> E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
120 119 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X = 2 ) -> E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
121 109 120 jca 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X = 2 ) -> ( { <. 1 , 1 >. , <. 1 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
122 fveq2 
 |-  ( X = 2 -> ( F ` X ) = ( F ` 2 ) )
123 1 fveq1i 
 |-  ( F ` 2 ) = ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 2 )
124 prex 
 |-  { <. 1 , 1 >. , <. 1 , 0 >. } e. _V
125 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 >. } )
126 124 125 ax-mp 
 |-  ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 2 ) = { <. 1 , 1 >. , <. 1 , 0 >. }
127 123 126 eqtri 
 |-  ( F ` 2 ) = { <. 1 , 1 >. , <. 1 , 0 >. }
128 122 127 eqtrdi 
 |-  ( X = 2 -> ( F ` X ) = { <. 1 , 1 >. , <. 1 , 0 >. } )
129 128 eleq1d 
 |-  ( X = 2 -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) <-> { <. 1 , 1 >. , <. 1 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
130 128 eqeq1d 
 |-  ( X = 2 -> ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) )
131 128 eqeq1d 
 |-  ( X = 2 -> ( ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } <-> { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } ) )
132 128 eqeq1d 
 |-  ( X = 2 -> ( ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
133 130 131 132 3orbi123d 
 |-  ( X = 2 -> ( ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
134 133 rexbidv 
 |-  ( X = 2 -> ( 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 ) >. } ) <-> E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
135 129 134 anbi12d 
 |-  ( X = 2 -> ( ( ( 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 ) >. } ) ) <-> ( { <. 1 , 1 >. , <. 1 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
136 135 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X = 2 ) -> ( ( ( 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 ) >. } ) ) <-> ( { <. 1 , 1 >. , <. 1 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
137 121 136 mpbird 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X = 2 ) -> ( ( 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 ) >. } ) ) )
138 137 expcom 
 |-  ( X = 2 -> ( N e. ( ZZ>= ` 3 ) -> ( ( 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 ) >. } ) ) ) )
139 prelpwi 
 |-  ( ( <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 0 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) -> { <. 1 , 0 >. , <. 0 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) )
140 105 13 139 syl2anc 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 0 >. , <. 0 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) )
141 28 eqeq2d 
 |-  ( x = 0 -> ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } ) )
142 31 eqeq2d 
 |-  ( x = 0 -> ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } <-> { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } ) )
143 34 eqeq2d 
 |-  ( x = 0 -> ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) )
144 141 142 143 3orbi123d 
 |-  ( x = 0 -> ( ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) ) )
145 prcom 
 |-  { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. }
146 145 3mix2i 
 |-  ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } )
147 146 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) )
148 144 12 147 rspcedvdw 
 |-  ( N e. ( ZZ>= ` 3 ) -> E. x e. ( 0 ..^ N ) ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
149 140 148 jca 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 0 >. , <. 0 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
150 fveq2 
 |-  ( X = 3 -> ( F ` X ) = ( F ` 3 ) )
151 1 fveq1i 
 |-  ( F ` 3 ) = ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 3 )
152 prex 
 |-  { <. 1 , 0 >. , <. 0 , 0 >. } e. _V
153 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 >. } )
154 152 153 ax-mp 
 |-  ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 3 ) = { <. 1 , 0 >. , <. 0 , 0 >. }
155 151 154 eqtri 
 |-  ( F ` 3 ) = { <. 1 , 0 >. , <. 0 , 0 >. }
156 150 155 eqtrdi 
 |-  ( X = 3 -> ( F ` X ) = { <. 1 , 0 >. , <. 0 , 0 >. } )
157 156 eleq1d 
 |-  ( X = 3 -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) <-> { <. 1 , 0 >. , <. 0 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
158 156 eqeq1d 
 |-  ( X = 3 -> ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) )
159 156 eqeq1d 
 |-  ( X = 3 -> ( ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } <-> { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } ) )
160 156 eqeq1d 
 |-  ( X = 3 -> ( ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
161 158 159 160 3orbi123d 
 |-  ( X = 3 -> ( ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
162 161 rexbidv 
 |-  ( X = 3 -> ( 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 ) >. } ) <-> E. x e. ( 0 ..^ N ) ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
163 157 162 anbi12d 
 |-  ( X = 3 -> ( ( ( 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 ) >. } ) ) <-> ( { <. 1 , 0 >. , <. 0 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
164 149 163 imbitrrid 
 |-  ( X = 3 -> ( N e. ( ZZ>= ` 3 ) -> ( ( 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 ) >. } ) ) ) )
165 138 164 jaoi 
 |-  ( ( X = 2 \/ X = 3 ) -> ( N e. ( ZZ>= ` 3 ) -> ( ( 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 ) >. } ) ) ) )
166 104 165 syl 
 |-  ( X e. { 2 , 3 } -> ( N e. ( ZZ>= ` 3 ) -> ( ( 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 ) >. } ) ) ) )
167 103 166 jaoi 
 |-  ( ( X e. { 0 , 1 } \/ X e. { 2 , 3 } ) -> ( N e. ( ZZ>= ` 3 ) -> ( ( 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 ) >. } ) ) ) )
168 5 167 sylbi 
 |-  ( X e. ( 0 ..^ 4 ) -> ( N e. ( ZZ>= ` 3 ) -> ( ( 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 ) >. } ) ) ) )
169 168 impcom 
 |-  ( ( 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 ) >. } ) ) )