Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . 5
⊢ (𝑣 = 𝑉 → (ℤ ↑𝑚
𝑣) = (ℤ
↑𝑚 𝑉)) |
2 | 1 | oveq2d 6666 |
. . . 4
⊢ (𝑣 = 𝑉 → (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣)) = (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉))) |
3 | 2 | pweqd 4163 |
. . 3
⊢ (𝑣 = 𝑉 → 𝒫 (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) = 𝒫 (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉))) |
4 | 1 | xpeq1d 5138 |
. . . . . . . 8
⊢ (𝑣 = 𝑉 → ((ℤ ↑𝑚
𝑣) × {𝑎}) = ((ℤ
↑𝑚 𝑉) × {𝑎})) |
5 | 4 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑣 = 𝑉 → (((ℤ
↑𝑚 𝑣) × {𝑎}) ∈ 𝑝 ↔ ((ℤ ↑𝑚
𝑉) × {𝑎}) ∈ 𝑝)) |
6 | 5 | ralbidv 2986 |
. . . . . 6
⊢ (𝑣 = 𝑉 → (∀𝑎 ∈ ℤ ((ℤ
↑𝑚 𝑣) × {𝑎}) ∈ 𝑝 ↔ ∀𝑎 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑎}) ∈ 𝑝)) |
7 | | sneq 4187 |
. . . . . . . . 9
⊢ (𝑎 = 𝑖 → {𝑎} = {𝑖}) |
8 | 7 | xpeq2d 5139 |
. . . . . . . 8
⊢ (𝑎 = 𝑖 → ((ℤ ↑𝑚
𝑉) × {𝑎}) = ((ℤ
↑𝑚 𝑉) × {𝑖})) |
9 | 8 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑎 = 𝑖 → (((ℤ ↑𝑚
𝑉) × {𝑎}) ∈ 𝑝 ↔ ((ℤ ↑𝑚
𝑉) × {𝑖}) ∈ 𝑝)) |
10 | 9 | cbvralv 3171 |
. . . . . 6
⊢
(∀𝑎 ∈
ℤ ((ℤ ↑𝑚 𝑉) × {𝑎}) ∈ 𝑝 ↔ ∀𝑖 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑖}) ∈ 𝑝) |
11 | 6, 10 | syl6bb 276 |
. . . . 5
⊢ (𝑣 = 𝑉 → (∀𝑎 ∈ ℤ ((ℤ
↑𝑚 𝑣) × {𝑎}) ∈ 𝑝 ↔ ∀𝑖 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑖}) ∈ 𝑝)) |
12 | 1 | mpteq1d 4738 |
. . . . . . . 8
⊢ (𝑣 = 𝑉 → (𝑐 ∈ (ℤ ↑𝑚
𝑣) ↦ (𝑐‘𝑏)) = (𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏))) |
13 | 12 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑣 = 𝑉 → ((𝑐 ∈ (ℤ ↑𝑚
𝑣) ↦ (𝑐‘𝑏)) ∈ 𝑝 ↔ (𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏)) ∈ 𝑝)) |
14 | 13 | raleqbi1dv 3146 |
. . . . . 6
⊢ (𝑣 = 𝑉 → (∀𝑏 ∈ 𝑣 (𝑐 ∈ (ℤ ↑𝑚
𝑣) ↦ (𝑐‘𝑏)) ∈ 𝑝 ↔ ∀𝑏 ∈ 𝑉 (𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏)) ∈ 𝑝)) |
15 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑗 → (𝑐‘𝑏) = (𝑐‘𝑗)) |
16 | 15 | mpteq2dv 4745 |
. . . . . . . . 9
⊢ (𝑏 = 𝑗 → (𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏)) = (𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑗))) |
17 | 16 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑏 = 𝑗 → ((𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏)) ∈ 𝑝 ↔ (𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑗)) ∈ 𝑝)) |
18 | | fveq1 6190 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑥 → (𝑐‘𝑗) = (𝑥‘𝑗)) |
19 | 18 | cbvmptv 4750 |
. . . . . . . . 9
⊢ (𝑐 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑐‘𝑗)) = (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑥‘𝑗)) |
20 | 19 | eleq1i 2692 |
. . . . . . . 8
⊢ ((𝑐 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑐‘𝑗)) ∈ 𝑝 ↔ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝) |
21 | 17, 20 | syl6bb 276 |
. . . . . . 7
⊢ (𝑏 = 𝑗 → ((𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏)) ∈ 𝑝 ↔ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝)) |
22 | 21 | cbvralv 3171 |
. . . . . 6
⊢
(∀𝑏 ∈
𝑉 (𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏)) ∈ 𝑝 ↔ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝) |
23 | 14, 22 | syl6bb 276 |
. . . . 5
⊢ (𝑣 = 𝑉 → (∀𝑏 ∈ 𝑣 (𝑐 ∈ (ℤ ↑𝑚
𝑣) ↦ (𝑐‘𝑏)) ∈ 𝑝 ↔ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝)) |
24 | 11, 23 | anbi12d 747 |
. . . 4
⊢ (𝑣 = 𝑉 → ((∀𝑎 ∈ ℤ ((ℤ
↑𝑚 𝑣) × {𝑎}) ∈ 𝑝 ∧ ∀𝑏 ∈ 𝑣 (𝑐 ∈ (ℤ ↑𝑚
𝑣) ↦ (𝑐‘𝑏)) ∈ 𝑝) ↔ (∀𝑖 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝))) |
25 | 24 | anbi1d 741 |
. . 3
⊢ (𝑣 = 𝑉 → (((∀𝑎 ∈ ℤ ((ℤ
↑𝑚 𝑣) × {𝑎}) ∈ 𝑝 ∧ ∀𝑏 ∈ 𝑣 (𝑐 ∈ (ℤ ↑𝑚
𝑣) ↦ (𝑐‘𝑏)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑝)) ↔ ((∀𝑖 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑝)))) |
26 | 3, 25 | rabeqbidv 3195 |
. 2
⊢ (𝑣 = 𝑉 → {𝑝 ∈ 𝒫 (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ∣ ((∀𝑎 ∈ ℤ ((ℤ
↑𝑚 𝑣) × {𝑎}) ∈ 𝑝 ∧ ∀𝑏 ∈ 𝑣 (𝑐 ∈ (ℤ ↑𝑚
𝑣) ↦ (𝑐‘𝑏)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑝))} = {𝑝 ∈ 𝒫 (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∣ ((∀𝑖 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑝))}) |
27 | | df-mzpcl 37286 |
. 2
⊢ mzPolyCld
= (𝑣 ∈ V ↦
{𝑝 ∈ 𝒫
(ℤ ↑𝑚 (ℤ ↑𝑚 𝑣)) ∣ ((∀𝑎 ∈ ℤ ((ℤ
↑𝑚 𝑣) × {𝑎}) ∈ 𝑝 ∧ ∀𝑏 ∈ 𝑣 (𝑐 ∈ (ℤ ↑𝑚
𝑣) ↦ (𝑐‘𝑏)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑝))}) |
28 | | ovex 6678 |
. . . 4
⊢ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∈ V |
29 | 28 | pwex 4848 |
. . 3
⊢ 𝒫
(ℤ ↑𝑚 (ℤ ↑𝑚 𝑉)) ∈ V |
30 | 29 | rabex 4813 |
. 2
⊢ {𝑝 ∈ 𝒫 (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∣ ((∀𝑖 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑝))} ∈ V |
31 | 26, 27, 30 | fvmpt 6282 |
1
⊢ (𝑉 ∈ V →
(mzPolyCld‘𝑉) =
{𝑝 ∈ 𝒫
(ℤ ↑𝑚 (ℤ ↑𝑚 𝑉)) ∣ ((∀𝑖 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑝))}) |