Proof of Theorem gpgiedg
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | gpgov.j |
. . . 4
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2))) |
| 2 | | gpgov.i |
. . . 4
⊢ 𝐼 = (0..^𝑁) |
| 3 | 1, 2 | gpgov 48006 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (𝑁 gPetersenGr 𝐾) = {⟨(Base‘ndx), ({0, 1} ×
𝐼)⟩,
⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 ({0, 1} × 𝐼) ∣ ∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})})⟩}) |
| 4 | 3 | fveq2d 6844 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (iEdg‘(𝑁 gPetersenGr 𝐾)) = (iEdg‘{⟨(Base‘ndx),
({0, 1} × 𝐼)⟩,
⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 ({0, 1} × 𝐼) ∣ ∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})})⟩})) |
| 5 | | prex 5387 |
. . . . 5
⊢ {0, 1}
∈ V |
| 6 | 2 | ovexi 7403 |
. . . . 5
⊢ 𝐼 ∈ V |
| 7 | 5, 6 | xpex 7709 |
. . . 4
⊢ ({0, 1}
× 𝐼) ∈
V |
| 8 | | eqid 2729 |
. . . . . . 7
⊢ {𝑒 ∈ 𝒫 ({0, 1}
× 𝐼) ∣
∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})} = {𝑒 ∈ 𝒫 ({0, 1} × 𝐼) ∣ ∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})} |
| 9 | 5 | a1i 11 |
. . . . . . . . 9
⊢ (𝐼 = (0..^𝑁) → {0, 1} ∈ V) |
| 10 | | ovexd 7404 |
. . . . . . . . . 10
⊢ (𝐼 = (0..^𝑁) → (0..^𝑁) ∈ V) |
| 11 | 2, 10 | eqeltrid 2832 |
. . . . . . . . 9
⊢ (𝐼 = (0..^𝑁) → 𝐼 ∈ V) |
| 12 | 9, 11 | xpexd 7707 |
. . . . . . . 8
⊢ (𝐼 = (0..^𝑁) → ({0, 1} × 𝐼) ∈ V) |
| 13 | 12 | pwexd 5329 |
. . . . . . 7
⊢ (𝐼 = (0..^𝑁) → 𝒫 ({0, 1} × 𝐼) ∈ V) |
| 14 | 8, 13 | rabexd 5290 |
. . . . . 6
⊢ (𝐼 = (0..^𝑁) → {𝑒 ∈ 𝒫 ({0, 1} × 𝐼) ∣ ∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})} ∈ V) |
| 15 | 14 | resiexd 7172 |
. . . . 5
⊢ (𝐼 = (0..^𝑁) → ( I ↾ {𝑒 ∈ 𝒫 ({0, 1} × 𝐼) ∣ ∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})}) ∈ V) |
| 16 | 2, 15 | ax-mp 5 |
. . . 4
⊢ ( I
↾ {𝑒 ∈ 𝒫
({0, 1} × 𝐼) ∣
∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})}) ∈ V |
| 17 | 7, 16 | pm3.2i 470 |
. . 3
⊢ (({0, 1}
× 𝐼) ∈ V ∧ (
I ↾ {𝑒 ∈
𝒫 ({0, 1} × 𝐼) ∣ ∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})}) ∈ V) |
| 18 | | eqid 2729 |
. . . 4
⊢
{⟨(Base‘ndx), ({0, 1} × 𝐼)⟩, ⟨(.ef‘ndx), ( I ↾
{𝑒 ∈ 𝒫 ({0, 1}
× 𝐼) ∣
∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})})⟩} =
{⟨(Base‘ndx), ({0, 1} × 𝐼)⟩, ⟨(.ef‘ndx), ( I ↾
{𝑒 ∈ 𝒫 ({0, 1}
× 𝐼) ∣
∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})})⟩} |
| 19 | 18 | struct2griedg 28931 |
. . 3
⊢ ((({0, 1}
× 𝐼) ∈ V ∧ (
I ↾ {𝑒 ∈
𝒫 ({0, 1} × 𝐼) ∣ ∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})}) ∈ V) →
(iEdg‘{⟨(Base‘ndx), ({0, 1} × 𝐼)⟩, ⟨(.ef‘ndx), ( I ↾
{𝑒 ∈ 𝒫 ({0, 1}
× 𝐼) ∣
∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})})⟩}) = ( I ↾ {𝑒 ∈ 𝒫 ({0, 1}
× 𝐼) ∣
∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})})) |
| 20 | 17, 19 | mp1i 13 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) →
(iEdg‘{⟨(Base‘ndx), ({0, 1} × 𝐼)⟩, ⟨(.ef‘ndx), ( I ↾
{𝑒 ∈ 𝒫 ({0, 1}
× 𝐼) ∣
∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})})⟩}) = ( I ↾ {𝑒 ∈ 𝒫 ({0, 1}
× 𝐼) ∣
∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})})) |
| 21 | 4, 20 | eqtrd 2764 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (iEdg‘(𝑁 gPetersenGr 𝐾)) = ( I ↾ {𝑒 ∈ 𝒫 ({0, 1} × 𝐼) ∣ ∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})})) |
