| Step |
Hyp |
Ref |
Expression |
| 1 |
|
gpgprismgr4cycl.p |
⊢ 𝑃 = ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ |
| 2 |
|
gpgprismgr4cycl.f |
⊢ 𝐹 = ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩ |
| 3 |
|
gpgprismgr4cycl.g |
⊢ 𝐺 = ( 𝑁 gPetersenGr 1 ) |
| 4 |
3
|
fveq2i |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) |
| 5 |
4
|
a1i |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( iEdg ‘ 𝐺 ) = ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ) |
| 6 |
|
eluzge3nn |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ ) |
| 7 |
|
1elfzo1ceilhalf1 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) |
| 8 |
6 7
|
jca |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 ∈ ℕ ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) ) |
| 9 |
8
|
adantr |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑁 ∈ ℕ ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) ) |
| 10 |
|
eqid |
⊢ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) |
| 11 |
|
eqid |
⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 ) |
| 12 |
10 11
|
gpgiedg |
⊢ ( ( 𝑁 ∈ ℕ ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) = ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) } ) ) |
| 13 |
9 12
|
syl |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) = ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) } ) ) |
| 14 |
5 13
|
eqtrd |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( iEdg ‘ 𝐺 ) = ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) } ) ) |
| 15 |
14
|
fveq1d |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑋 ) ) = ( ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) } ) ‘ ( 𝐹 ‘ 𝑋 ) ) ) |
| 16 |
2
|
gpgprismgr4cycllem3 |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑋 ∈ ( 0 ..^ 4 ) ) → ( ( 𝐹 ‘ 𝑋 ) ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐹 ‘ 𝑋 ) = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ ( 𝐹 ‘ 𝑋 ) = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ ( 𝐹 ‘ 𝑋 ) = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ) ) |
| 17 |
2
|
gpgprismgr4cycllem1 |
⊢ ( ♯ ‘ 𝐹 ) = 4 |
| 18 |
17
|
oveq2i |
⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) |
| 19 |
18
|
eleq2i |
⊢ ( 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ 𝑋 ∈ ( 0 ..^ 4 ) ) |
| 20 |
19
|
anbi2i |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑋 ∈ ( 0 ..^ 4 ) ) ) |
| 21 |
|
eqeq1 |
⊢ ( 𝑒 = ( 𝐹 ‘ 𝑋 ) → ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ↔ ( 𝐹 ‘ 𝑋 ) = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ) |
| 22 |
|
eqeq1 |
⊢ ( 𝑒 = ( 𝐹 ‘ 𝑋 ) → ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ↔ ( 𝐹 ‘ 𝑋 ) = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ) ) |
| 23 |
|
eqeq1 |
⊢ ( 𝑒 = ( 𝐹 ‘ 𝑋 ) → ( 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ↔ ( 𝐹 ‘ 𝑋 ) = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ) |
| 24 |
21 22 23
|
3orbi123d |
⊢ ( 𝑒 = ( 𝐹 ‘ 𝑋 ) → ( ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ↔ ( ( 𝐹 ‘ 𝑋 ) = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ ( 𝐹 ‘ 𝑋 ) = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ ( 𝐹 ‘ 𝑋 ) = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ) ) |
| 25 |
24
|
rexbidv |
⊢ ( 𝑒 = ( 𝐹 ‘ 𝑋 ) → ( ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ↔ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐹 ‘ 𝑋 ) = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ ( 𝐹 ‘ 𝑋 ) = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ ( 𝐹 ‘ 𝑋 ) = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ) ) |
| 26 |
25
|
elrab |
⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) } ↔ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐹 ‘ 𝑋 ) = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ ( 𝐹 ‘ 𝑋 ) = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ ( 𝐹 ‘ 𝑋 ) = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ) ) |
| 27 |
16 20 26
|
3imtr4i |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 𝑋 ) ∈ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) } ) |
| 28 |
|
fvresi |
⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) } → ( ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) } ) ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) ) |
| 29 |
27 28
|
syl |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) } ) ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) ) |
| 30 |
15 29
|
eqtrd |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) ) |
| 31 |
|
fzo0to42pr |
⊢ ( 0 ..^ 4 ) = ( { 0 , 1 } ∪ { 2 , 3 } ) |
| 32 |
31
|
eleq2i |
⊢ ( 𝑋 ∈ ( 0 ..^ 4 ) ↔ 𝑋 ∈ ( { 0 , 1 } ∪ { 2 , 3 } ) ) |
| 33 |
|
elun |
⊢ ( 𝑋 ∈ ( { 0 , 1 } ∪ { 2 , 3 } ) ↔ ( 𝑋 ∈ { 0 , 1 } ∨ 𝑋 ∈ { 2 , 3 } ) ) |
| 34 |
19 32 33
|
3bitri |
⊢ ( 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑋 ∈ { 0 , 1 } ∨ 𝑋 ∈ { 2 , 3 } ) ) |
| 35 |
|
elpri |
⊢ ( 𝑋 ∈ { 0 , 1 } → ( 𝑋 = 0 ∨ 𝑋 = 1 ) ) |
| 36 |
|
prex |
⊢ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ V |
| 37 |
|
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 ⟩ } ) |
| 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 |
⊢ ( 𝐹 ‘ 0 ) = ( ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩ ‘ 0 ) |
| 40 |
1
|
fveq1i |
⊢ ( 𝑃 ‘ 0 ) = ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ‘ 0 ) |
| 41 |
|
opex |
⊢ ⟨ 0 , 0 ⟩ ∈ 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 ⟩ ”⟩ ∈ Word V |
| 44 |
|
s4len |
⊢ ( ♯ ‘ ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ”⟩ ) = 4 |
| 45 |
|
s4fv0 |
⊢ ( ⟨ 0 , 0 ⟩ ∈ V → ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ”⟩ ‘ 0 ) = ⟨ 0 , 0 ⟩ ) |
| 46 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
| 47 |
|
4pos |
⊢ 0 < 4 |
| 48 |
42 43 44 45 46 47
|
cats1fv |
⊢ ( ⟨ 0 , 0 ⟩ ∈ 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 |
⊢ ( 𝑃 ‘ 0 ) = ⟨ 0 , 0 ⟩ |
| 51 |
1
|
fveq1i |
⊢ ( 𝑃 ‘ 1 ) = ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ‘ 1 ) |
| 52 |
|
opex |
⊢ ⟨ 0 , 1 ⟩ ∈ V |
| 53 |
|
s4fv1 |
⊢ ( ⟨ 0 , 1 ⟩ ∈ V → ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ”⟩ ‘ 1 ) = ⟨ 0 , 1 ⟩ ) |
| 54 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
| 55 |
|
1lt4 |
⊢ 1 < 4 |
| 56 |
42 43 44 53 54 55
|
cats1fv |
⊢ ( ⟨ 0 , 1 ⟩ ∈ 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 |
⊢ ( 𝑃 ‘ 1 ) = ⟨ 0 , 1 ⟩ |
| 59 |
50 58
|
preq12i |
⊢ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } = { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } |
| 60 |
38 39 59
|
3eqtr4i |
⊢ ( 𝐹 ‘ 0 ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } |
| 61 |
|
fveq2 |
⊢ ( 𝑋 = 0 → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 0 ) ) |
| 62 |
|
fveq2 |
⊢ ( 𝑋 = 0 → ( 𝑃 ‘ 𝑋 ) = ( 𝑃 ‘ 0 ) ) |
| 63 |
|
fv0p1e1 |
⊢ ( 𝑋 = 0 → ( 𝑃 ‘ ( 𝑋 + 1 ) ) = ( 𝑃 ‘ 1 ) ) |
| 64 |
62 63
|
preq12d |
⊢ ( 𝑋 = 0 → { ( 𝑃 ‘ 𝑋 ) , ( 𝑃 ‘ ( 𝑋 + 1 ) ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) |
| 65 |
60 61 64
|
3eqtr4a |
⊢ ( 𝑋 = 0 → ( 𝐹 ‘ 𝑋 ) = { ( 𝑃 ‘ 𝑋 ) , ( 𝑃 ‘ ( 𝑋 + 1 ) ) } ) |
| 66 |
|
prex |
⊢ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ V |
| 67 |
|
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 ⟩ } ) |
| 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 |
⊢ ( 𝐹 ‘ 1 ) = ( ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩ ‘ 1 ) |
| 70 |
1
|
fveq1i |
⊢ ( 𝑃 ‘ 2 ) = ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ‘ 2 ) |
| 71 |
|
opex |
⊢ ⟨ 1 , 1 ⟩ ∈ V |
| 72 |
|
s4fv2 |
⊢ ( ⟨ 1 , 1 ⟩ ∈ V → ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ”⟩ ‘ 2 ) = ⟨ 1 , 1 ⟩ ) |
| 73 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
| 74 |
|
2lt4 |
⊢ 2 < 4 |
| 75 |
42 43 44 72 73 74
|
cats1fv |
⊢ ( ⟨ 1 , 1 ⟩ ∈ 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 |
⊢ ( 𝑃 ‘ 2 ) = ⟨ 1 , 1 ⟩ |
| 78 |
58 77
|
preq12i |
⊢ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } = { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } |
| 79 |
68 69 78
|
3eqtr4i |
⊢ ( 𝐹 ‘ 1 ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } |
| 80 |
|
fveq2 |
⊢ ( 𝑋 = 1 → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 1 ) ) |
| 81 |
|
fveq2 |
⊢ ( 𝑋 = 1 → ( 𝑃 ‘ 𝑋 ) = ( 𝑃 ‘ 1 ) ) |
| 82 |
|
oveq1 |
⊢ ( 𝑋 = 1 → ( 𝑋 + 1 ) = ( 1 + 1 ) ) |
| 83 |
|
1p1e2 |
⊢ ( 1 + 1 ) = 2 |
| 84 |
82 83
|
eqtrdi |
⊢ ( 𝑋 = 1 → ( 𝑋 + 1 ) = 2 ) |
| 85 |
84
|
fveq2d |
⊢ ( 𝑋 = 1 → ( 𝑃 ‘ ( 𝑋 + 1 ) ) = ( 𝑃 ‘ 2 ) ) |
| 86 |
81 85
|
preq12d |
⊢ ( 𝑋 = 1 → { ( 𝑃 ‘ 𝑋 ) , ( 𝑃 ‘ ( 𝑋 + 1 ) ) } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) |
| 87 |
79 80 86
|
3eqtr4a |
⊢ ( 𝑋 = 1 → ( 𝐹 ‘ 𝑋 ) = { ( 𝑃 ‘ 𝑋 ) , ( 𝑃 ‘ ( 𝑋 + 1 ) ) } ) |
| 88 |
65 87
|
jaoi |
⊢ ( ( 𝑋 = 0 ∨ 𝑋 = 1 ) → ( 𝐹 ‘ 𝑋 ) = { ( 𝑃 ‘ 𝑋 ) , ( 𝑃 ‘ ( 𝑋 + 1 ) ) } ) |
| 89 |
35 88
|
syl |
⊢ ( 𝑋 ∈ { 0 , 1 } → ( 𝐹 ‘ 𝑋 ) = { ( 𝑃 ‘ 𝑋 ) , ( 𝑃 ‘ ( 𝑋 + 1 ) ) } ) |
| 90 |
|
elpri |
⊢ ( 𝑋 ∈ { 2 , 3 } → ( 𝑋 = 2 ∨ 𝑋 = 3 ) ) |
| 91 |
|
prex |
⊢ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ V |
| 92 |
|
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 ⟩ } ) |
| 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 |
⊢ ( 𝐹 ‘ 2 ) = ( ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩ ‘ 2 ) |
| 95 |
1
|
fveq1i |
⊢ ( 𝑃 ‘ 3 ) = ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ‘ 3 ) |
| 96 |
|
opex |
⊢ ⟨ 1 , 0 ⟩ ∈ V |
| 97 |
|
s4fv3 |
⊢ ( ⟨ 1 , 0 ⟩ ∈ V → ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ”⟩ ‘ 3 ) = ⟨ 1 , 0 ⟩ ) |
| 98 |
|
3nn0 |
⊢ 3 ∈ ℕ0 |
| 99 |
|
3lt4 |
⊢ 3 < 4 |
| 100 |
42 43 44 97 98 99
|
cats1fv |
⊢ ( ⟨ 1 , 0 ⟩ ∈ 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 |
⊢ ( 𝑃 ‘ 3 ) = ⟨ 1 , 0 ⟩ |
| 103 |
77 102
|
preq12i |
⊢ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } = { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } |
| 104 |
93 94 103
|
3eqtr4i |
⊢ ( 𝐹 ‘ 2 ) = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } |
| 105 |
|
fveq2 |
⊢ ( 𝑋 = 2 → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 2 ) ) |
| 106 |
|
fveq2 |
⊢ ( 𝑋 = 2 → ( 𝑃 ‘ 𝑋 ) = ( 𝑃 ‘ 2 ) ) |
| 107 |
|
oveq1 |
⊢ ( 𝑋 = 2 → ( 𝑋 + 1 ) = ( 2 + 1 ) ) |
| 108 |
|
2p1e3 |
⊢ ( 2 + 1 ) = 3 |
| 109 |
107 108
|
eqtrdi |
⊢ ( 𝑋 = 2 → ( 𝑋 + 1 ) = 3 ) |
| 110 |
109
|
fveq2d |
⊢ ( 𝑋 = 2 → ( 𝑃 ‘ ( 𝑋 + 1 ) ) = ( 𝑃 ‘ 3 ) ) |
| 111 |
106 110
|
preq12d |
⊢ ( 𝑋 = 2 → { ( 𝑃 ‘ 𝑋 ) , ( 𝑃 ‘ ( 𝑋 + 1 ) ) } = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ) |
| 112 |
104 105 111
|
3eqtr4a |
⊢ ( 𝑋 = 2 → ( 𝐹 ‘ 𝑋 ) = { ( 𝑃 ‘ 𝑋 ) , ( 𝑃 ‘ ( 𝑋 + 1 ) ) } ) |
| 113 |
|
prex |
⊢ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∈ V |
| 114 |
|
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 ⟩ } ) |
| 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 |
⊢ ( 𝐹 ‘ 3 ) = ( ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩ ‘ 3 ) |
| 117 |
1
|
fveq1i |
⊢ ( 𝑃 ‘ 4 ) = ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ‘ 4 ) |
| 118 |
42 43 44
|
cats1fvn |
⊢ ( ⟨ 0 , 0 ⟩ ∈ 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 |
⊢ ( 𝑃 ‘ 4 ) = ⟨ 0 , 0 ⟩ |
| 121 |
102 120
|
preq12i |
⊢ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 4 ) } = { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } |
| 122 |
115 116 121
|
3eqtr4i |
⊢ ( 𝐹 ‘ 3 ) = { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 4 ) } |
| 123 |
|
fveq2 |
⊢ ( 𝑋 = 3 → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 3 ) ) |
| 124 |
|
fveq2 |
⊢ ( 𝑋 = 3 → ( 𝑃 ‘ 𝑋 ) = ( 𝑃 ‘ 3 ) ) |
| 125 |
|
oveq1 |
⊢ ( 𝑋 = 3 → ( 𝑋 + 1 ) = ( 3 + 1 ) ) |
| 126 |
|
3p1e4 |
⊢ ( 3 + 1 ) = 4 |
| 127 |
125 126
|
eqtrdi |
⊢ ( 𝑋 = 3 → ( 𝑋 + 1 ) = 4 ) |
| 128 |
127
|
fveq2d |
⊢ ( 𝑋 = 3 → ( 𝑃 ‘ ( 𝑋 + 1 ) ) = ( 𝑃 ‘ 4 ) ) |
| 129 |
124 128
|
preq12d |
⊢ ( 𝑋 = 3 → { ( 𝑃 ‘ 𝑋 ) , ( 𝑃 ‘ ( 𝑋 + 1 ) ) } = { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 4 ) } ) |
| 130 |
122 123 129
|
3eqtr4a |
⊢ ( 𝑋 = 3 → ( 𝐹 ‘ 𝑋 ) = { ( 𝑃 ‘ 𝑋 ) , ( 𝑃 ‘ ( 𝑋 + 1 ) ) } ) |
| 131 |
112 130
|
jaoi |
⊢ ( ( 𝑋 = 2 ∨ 𝑋 = 3 ) → ( 𝐹 ‘ 𝑋 ) = { ( 𝑃 ‘ 𝑋 ) , ( 𝑃 ‘ ( 𝑋 + 1 ) ) } ) |
| 132 |
90 131
|
syl |
⊢ ( 𝑋 ∈ { 2 , 3 } → ( 𝐹 ‘ 𝑋 ) = { ( 𝑃 ‘ 𝑋 ) , ( 𝑃 ‘ ( 𝑋 + 1 ) ) } ) |
| 133 |
89 132
|
jaoi |
⊢ ( ( 𝑋 ∈ { 0 , 1 } ∨ 𝑋 ∈ { 2 , 3 } ) → ( 𝐹 ‘ 𝑋 ) = { ( 𝑃 ‘ 𝑋 ) , ( 𝑃 ‘ ( 𝑋 + 1 ) ) } ) |
| 134 |
34 133
|
sylbi |
⊢ ( 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 𝑋 ) = { ( 𝑃 ‘ 𝑋 ) , ( 𝑃 ‘ ( 𝑋 + 1 ) ) } ) |
| 135 |
134
|
adantl |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 𝑋 ) = { ( 𝑃 ‘ 𝑋 ) , ( 𝑃 ‘ ( 𝑋 + 1 ) ) } ) |
| 136 |
30 135
|
eqtrd |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑋 ) ) = { ( 𝑃 ‘ 𝑋 ) , ( 𝑃 ‘ ( 𝑋 + 1 ) ) } ) |