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