# Metamath Proof Explorer

## Theorem etransclem12

Description: C applied to N . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem12.1 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } )
etransclem12.2 ( 𝜑𝑁 ∈ ℕ0 )
Assertion etransclem12 ( 𝜑 → ( 𝐶𝑁 ) = { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑁 } )

### Proof

Step Hyp Ref Expression
1 etransclem12.1 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } )
2 etransclem12.2 ( 𝜑𝑁 ∈ ℕ0 )
3 oveq2 ( 𝑛 = 𝑁 → ( 0 ... 𝑛 ) = ( 0 ... 𝑁 ) )
4 3 oveq1d ( 𝑛 = 𝑁 → ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) = ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) )
5 eqeq2 ( 𝑛 = 𝑁 → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 ↔ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑁 ) )
6 4 5 rabeqbidv ( 𝑛 = 𝑁 → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑁 } )
7 ovex ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∈ V
8 7 rabex { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑁 } ∈ V
9 8 a1i ( 𝜑 → { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑁 } ∈ V )
10 1 6 2 9 fvmptd3 ( 𝜑 → ( 𝐶𝑁 ) = { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑁 } )