| Step | Hyp | Ref
| Expression |
| 1 | | df-stgr 47919 |
. . 3
⊢ StarGr =
(𝑛 ∈
ℕ0 ↦ {〈(Base‘ndx), (0...𝑛)〉, 〈(.ef‘ndx), ( I ↾
{𝑒 ∈ 𝒫
(0...𝑛) ∣
∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})〉}) |
| 2 | 1 | a1i 11 |
. 2
⊢ (𝑁 ∈ ℕ0
→ StarGr = (𝑛 ∈
ℕ0 ↦ {〈(Base‘ndx), (0...𝑛)〉, 〈(.ef‘ndx), ( I ↾
{𝑒 ∈ 𝒫
(0...𝑛) ∣
∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})〉})) |
| 3 | | oveq2 7439 |
. . . . 5
⊢ (𝑛 = 𝑁 → (0...𝑛) = (0...𝑁)) |
| 4 | 3 | opeq2d 4880 |
. . . 4
⊢ (𝑛 = 𝑁 → 〈(Base‘ndx), (0...𝑛)〉 =
〈(Base‘ndx), (0...𝑁)〉) |
| 5 | 3 | pweqd 4617 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → 𝒫 (0...𝑛) = 𝒫 (0...𝑁)) |
| 6 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (1...𝑛) = (1...𝑁)) |
| 7 | 6 | rexeqdv 3327 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥} ↔ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥})) |
| 8 | 5, 7 | rabeqbidv 3455 |
. . . . . 6
⊢ (𝑛 = 𝑁 → {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}} = {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}) |
| 9 | 8 | reseq2d 5997 |
. . . . 5
⊢ (𝑛 = 𝑁 → ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}}) = ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})) |
| 10 | 9 | opeq2d 4880 |
. . . 4
⊢ (𝑛 = 𝑁 → 〈(.ef‘ndx), ( I ↾
{𝑒 ∈ 𝒫
(0...𝑛) ∣
∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})〉 = 〈(.ef‘ndx), ( I
↾ {𝑒 ∈ 𝒫
(0...𝑁) ∣
∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})〉) |
| 11 | 4, 10 | preq12d 4741 |
. . 3
⊢ (𝑛 = 𝑁 → {〈(Base‘ndx), (0...𝑛)〉, 〈(.ef‘ndx),
( I ↾ {𝑒 ∈
𝒫 (0...𝑛) ∣
∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})〉} = {〈(Base‘ndx),
(0...𝑁)〉,
〈(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})〉}) |
| 12 | 11 | adantl 481 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 = 𝑁) → {〈(Base‘ndx), (0...𝑛)〉, 〈(.ef‘ndx),
( I ↾ {𝑒 ∈
𝒫 (0...𝑛) ∣
∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})〉} = {〈(Base‘ndx),
(0...𝑁)〉,
〈(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})〉}) |
| 13 | | id 22 |
. 2
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ0) |
| 14 | | prex 5437 |
. . 3
⊢
{〈(Base‘ndx), (0...𝑁)〉, 〈(.ef‘ndx), ( I ↾
{𝑒 ∈ 𝒫
(0...𝑁) ∣
∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})〉} ∈ V |
| 15 | 14 | a1i 11 |
. 2
⊢ (𝑁 ∈ ℕ0
→ {〈(Base‘ndx), (0...𝑁)〉, 〈(.ef‘ndx), ( I ↾
{𝑒 ∈ 𝒫
(0...𝑁) ∣
∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})〉} ∈ V) |
| 16 | 2, 12, 13, 15 | fvmptd 7023 |
1
⊢ (𝑁 ∈ ℕ0
→ (StarGr‘𝑁) =
{〈(Base‘ndx), (0...𝑁)〉, 〈(.ef‘ndx), ( I ↾
{𝑒 ∈ 𝒫
(0...𝑁) ∣
∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})〉}) |