Step |
Hyp |
Ref |
Expression |
1 |
|
reprval.a |
⊢ ( 𝜑 → 𝐴 ⊆ ℕ ) |
2 |
|
reprval.m |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
3 |
|
reprval.s |
⊢ ( 𝜑 → 𝑆 ∈ ℕ0 ) |
4 |
|
df-repr |
⊢ repr = ( 𝑠 ∈ ℕ0 ↦ ( 𝑏 ∈ 𝒫 ℕ , 𝑚 ∈ ℤ ↦ { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑠 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } ) ) |
5 |
|
oveq2 |
⊢ ( 𝑠 = 𝑆 → ( 0 ..^ 𝑠 ) = ( 0 ..^ 𝑆 ) ) |
6 |
5
|
oveq2d |
⊢ ( 𝑠 = 𝑆 → ( 𝑏 ↑m ( 0 ..^ 𝑠 ) ) = ( 𝑏 ↑m ( 0 ..^ 𝑆 ) ) ) |
7 |
5
|
sumeq1d |
⊢ ( 𝑠 = 𝑆 → Σ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 ) = Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) ) |
8 |
7
|
eqeq1d |
⊢ ( 𝑠 = 𝑆 → ( Σ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 ↔ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 ) ) |
9 |
6 8
|
rabeqbidv |
⊢ ( 𝑠 = 𝑆 → { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑠 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } = { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } ) |
10 |
9
|
mpoeq3dv |
⊢ ( 𝑠 = 𝑆 → ( 𝑏 ∈ 𝒫 ℕ , 𝑚 ∈ ℤ ↦ { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑠 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } ) = ( 𝑏 ∈ 𝒫 ℕ , 𝑚 ∈ ℤ ↦ { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } ) ) |
11 |
|
nnex |
⊢ ℕ ∈ V |
12 |
11
|
pwex |
⊢ 𝒫 ℕ ∈ V |
13 |
|
zex |
⊢ ℤ ∈ V |
14 |
12 13
|
mpoex |
⊢ ( 𝑏 ∈ 𝒫 ℕ , 𝑚 ∈ ℤ ↦ { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } ) ∈ V |
15 |
14
|
a1i |
⊢ ( 𝜑 → ( 𝑏 ∈ 𝒫 ℕ , 𝑚 ∈ ℤ ↦ { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } ) ∈ V ) |
16 |
4 10 3 15
|
fvmptd3 |
⊢ ( 𝜑 → ( repr ‘ 𝑆 ) = ( 𝑏 ∈ 𝒫 ℕ , 𝑚 ∈ ℤ ↦ { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } ) ) |
17 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝐴 ∧ 𝑚 = 𝑀 ) ) → 𝑏 = 𝐴 ) |
18 |
17
|
oveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝐴 ∧ 𝑚 = 𝑀 ) ) → ( 𝑏 ↑m ( 0 ..^ 𝑆 ) ) = ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) |
19 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝐴 ∧ 𝑚 = 𝑀 ) ) → 𝑚 = 𝑀 ) |
20 |
19
|
eqeq2d |
⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝐴 ∧ 𝑚 = 𝑀 ) ) → ( Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 ↔ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ) ) |
21 |
18 20
|
rabeqbidv |
⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝐴 ∧ 𝑚 = 𝑀 ) ) → { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ) |
22 |
11
|
a1i |
⊢ ( 𝜑 → ℕ ∈ V ) |
23 |
22 1
|
ssexd |
⊢ ( 𝜑 → 𝐴 ∈ V ) |
24 |
23 1
|
elpwd |
⊢ ( 𝜑 → 𝐴 ∈ 𝒫 ℕ ) |
25 |
|
ovex |
⊢ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∈ V |
26 |
25
|
rabex |
⊢ { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ∈ V |
27 |
26
|
a1i |
⊢ ( 𝜑 → { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ∈ V ) |
28 |
16 21 24 2 27
|
ovmpod |
⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ) |