| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . 5
⊢ (𝑣 = 𝑉 → (ℤ ↑m 𝑣) = (ℤ ↑m
𝑉)) |
| 2 | 1 | oveq2d 7447 |
. . . 4
⊢ (𝑣 = 𝑉 → (ℤ ↑m (ℤ
↑m 𝑣)) =
(ℤ ↑m (ℤ ↑m 𝑉))) |
| 3 | 2 | pweqd 4617 |
. . 3
⊢ (𝑣 = 𝑉 → 𝒫 (ℤ
↑m (ℤ ↑m 𝑣)) = 𝒫 (ℤ ↑m
(ℤ ↑m 𝑉))) |
| 4 | 1 | xpeq1d 5714 |
. . . . . . . 8
⊢ (𝑣 = 𝑉 → ((ℤ ↑m 𝑣) × {𝑎}) = ((ℤ ↑m 𝑉) × {𝑎})) |
| 5 | 4 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑣 = 𝑉 → (((ℤ ↑m 𝑣) × {𝑎}) ∈ 𝑝 ↔ ((ℤ ↑m 𝑉) × {𝑎}) ∈ 𝑝)) |
| 6 | 5 | ralbidv 3178 |
. . . . . 6
⊢ (𝑣 = 𝑉 → (∀𝑎 ∈ ℤ ((ℤ ↑m
𝑣) × {𝑎}) ∈ 𝑝 ↔ ∀𝑎 ∈ ℤ ((ℤ ↑m
𝑉) × {𝑎}) ∈ 𝑝)) |
| 7 | | sneq 4636 |
. . . . . . . . 9
⊢ (𝑎 = 𝑖 → {𝑎} = {𝑖}) |
| 8 | 7 | xpeq2d 5715 |
. . . . . . . 8
⊢ (𝑎 = 𝑖 → ((ℤ ↑m 𝑉) × {𝑎}) = ((ℤ ↑m 𝑉) × {𝑖})) |
| 9 | 8 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑎 = 𝑖 → (((ℤ ↑m 𝑉) × {𝑎}) ∈ 𝑝 ↔ ((ℤ ↑m 𝑉) × {𝑖}) ∈ 𝑝)) |
| 10 | 9 | cbvralvw 3237 |
. . . . . 6
⊢
(∀𝑎 ∈
ℤ ((ℤ ↑m 𝑉) × {𝑎}) ∈ 𝑝 ↔ ∀𝑖 ∈ ℤ ((ℤ ↑m
𝑉) × {𝑖}) ∈ 𝑝) |
| 11 | 6, 10 | bitrdi 287 |
. . . . 5
⊢ (𝑣 = 𝑉 → (∀𝑎 ∈ ℤ ((ℤ ↑m
𝑣) × {𝑎}) ∈ 𝑝 ↔ ∀𝑖 ∈ ℤ ((ℤ ↑m
𝑉) × {𝑖}) ∈ 𝑝)) |
| 12 | 1 | mpteq1d 5237 |
. . . . . . . 8
⊢ (𝑣 = 𝑉 → (𝑐 ∈ (ℤ ↑m 𝑣) ↦ (𝑐‘𝑏)) = (𝑐 ∈ (ℤ ↑m 𝑉) ↦ (𝑐‘𝑏))) |
| 13 | 12 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑣 = 𝑉 → ((𝑐 ∈ (ℤ ↑m 𝑣) ↦ (𝑐‘𝑏)) ∈ 𝑝 ↔ (𝑐 ∈ (ℤ ↑m 𝑉) ↦ (𝑐‘𝑏)) ∈ 𝑝)) |
| 14 | 13 | raleqbi1dv 3338 |
. . . . . 6
⊢ (𝑣 = 𝑉 → (∀𝑏 ∈ 𝑣 (𝑐 ∈ (ℤ ↑m 𝑣) ↦ (𝑐‘𝑏)) ∈ 𝑝 ↔ ∀𝑏 ∈ 𝑉 (𝑐 ∈ (ℤ ↑m 𝑉) ↦ (𝑐‘𝑏)) ∈ 𝑝)) |
| 15 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑗 → (𝑐‘𝑏) = (𝑐‘𝑗)) |
| 16 | 15 | mpteq2dv 5244 |
. . . . . . . . 9
⊢ (𝑏 = 𝑗 → (𝑐 ∈ (ℤ ↑m 𝑉) ↦ (𝑐‘𝑏)) = (𝑐 ∈ (ℤ ↑m 𝑉) ↦ (𝑐‘𝑗))) |
| 17 | 16 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑏 = 𝑗 → ((𝑐 ∈ (ℤ ↑m 𝑉) ↦ (𝑐‘𝑏)) ∈ 𝑝 ↔ (𝑐 ∈ (ℤ ↑m 𝑉) ↦ (𝑐‘𝑗)) ∈ 𝑝)) |
| 18 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑥 → (𝑐‘𝑗) = (𝑥‘𝑗)) |
| 19 | 18 | cbvmptv 5255 |
. . . . . . . . 9
⊢ (𝑐 ∈ (ℤ
↑m 𝑉)
↦ (𝑐‘𝑗)) = (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) |
| 20 | 19 | eleq1i 2832 |
. . . . . . . 8
⊢ ((𝑐 ∈ (ℤ
↑m 𝑉)
↦ (𝑐‘𝑗)) ∈ 𝑝 ↔ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝) |
| 21 | 17, 20 | bitrdi 287 |
. . . . . . 7
⊢ (𝑏 = 𝑗 → ((𝑐 ∈ (ℤ ↑m 𝑉) ↦ (𝑐‘𝑏)) ∈ 𝑝 ↔ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝)) |
| 22 | 21 | cbvralvw 3237 |
. . . . . 6
⊢
(∀𝑏 ∈
𝑉 (𝑐 ∈ (ℤ ↑m 𝑉) ↦ (𝑐‘𝑏)) ∈ 𝑝 ↔ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝) |
| 23 | 14, 22 | bitrdi 287 |
. . . . 5
⊢ (𝑣 = 𝑉 → (∀𝑏 ∈ 𝑣 (𝑐 ∈ (ℤ ↑m 𝑣) ↦ (𝑐‘𝑏)) ∈ 𝑝 ↔ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝)) |
| 24 | 11, 23 | anbi12d 632 |
. . . 4
⊢ (𝑣 = 𝑉 → ((∀𝑎 ∈ ℤ ((ℤ ↑m
𝑣) × {𝑎}) ∈ 𝑝 ∧ ∀𝑏 ∈ 𝑣 (𝑐 ∈ (ℤ ↑m 𝑣) ↦ (𝑐‘𝑏)) ∈ 𝑝) ↔ (∀𝑖 ∈ ℤ ((ℤ ↑m
𝑉) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝))) |
| 25 | 24 | anbi1d 631 |
. . 3
⊢ (𝑣 = 𝑉 → (((∀𝑎 ∈ ℤ ((ℤ ↑m
𝑣) × {𝑎}) ∈ 𝑝 ∧ ∀𝑏 ∈ 𝑣 (𝑐 ∈ (ℤ ↑m 𝑣) ↦ (𝑐‘𝑏)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝)) ↔ ((∀𝑖 ∈ ℤ ((ℤ ↑m
𝑉) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝)))) |
| 26 | 3, 25 | rabeqbidv 3455 |
. 2
⊢ (𝑣 = 𝑉 → {𝑝 ∈ 𝒫 (ℤ ↑m
(ℤ ↑m 𝑣)) ∣ ((∀𝑎 ∈ ℤ ((ℤ ↑m
𝑣) × {𝑎}) ∈ 𝑝 ∧ ∀𝑏 ∈ 𝑣 (𝑐 ∈ (ℤ ↑m 𝑣) ↦ (𝑐‘𝑏)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))} = {𝑝 ∈ 𝒫 (ℤ ↑m
(ℤ ↑m 𝑉)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m
𝑉) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))}) |
| 27 | | df-mzpcl 42734 |
. 2
⊢ mzPolyCld
= (𝑣 ∈ V ↦
{𝑝 ∈ 𝒫
(ℤ ↑m (ℤ ↑m 𝑣)) ∣ ((∀𝑎 ∈ ℤ ((ℤ ↑m
𝑣) × {𝑎}) ∈ 𝑝 ∧ ∀𝑏 ∈ 𝑣 (𝑐 ∈ (ℤ ↑m 𝑣) ↦ (𝑐‘𝑏)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))}) |
| 28 | | ovex 7464 |
. . . 4
⊢ (ℤ
↑m (ℤ ↑m 𝑉)) ∈ V |
| 29 | 28 | pwex 5380 |
. . 3
⊢ 𝒫
(ℤ ↑m (ℤ ↑m 𝑉)) ∈ V |
| 30 | 29 | rabex 5339 |
. 2
⊢ {𝑝 ∈ 𝒫 (ℤ
↑m (ℤ ↑m 𝑉)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m
𝑉) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))} ∈ V |
| 31 | 26, 27, 30 | fvmpt 7016 |
1
⊢ (𝑉 ∈ V →
(mzPolyCld‘𝑉) =
{𝑝 ∈ 𝒫
(ℤ ↑m (ℤ ↑m 𝑉)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m
𝑉) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))}) |