# Metamath Proof Explorer

## Theorem etransclem16

Description: Every element in the range of C is a finite set. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem16.c 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } )
etransclem16.n ( 𝜑𝑁 ∈ ℕ0 )
Assertion etransclem16 ( 𝜑 → ( 𝐶𝑁 ) ∈ Fin )

### Proof

Step Hyp Ref Expression
1 etransclem16.c 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } )
2 etransclem16.n ( 𝜑𝑁 ∈ ℕ0 )
3 1 2 etransclem12 ( 𝜑 → ( 𝐶𝑁 ) = { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑁 } )
4 fzfi ( 0 ... 𝑁 ) ∈ Fin
5 fzfi ( 0 ... 𝑀 ) ∈ Fin
6 mapfi ( ( ( 0 ... 𝑁 ) ∈ Fin ∧ ( 0 ... 𝑀 ) ∈ Fin ) → ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∈ Fin )
7 4 5 6 mp2an ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∈ Fin
8 ssrab2 { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑁 } ⊆ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) )
9 ssfi ( ( ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∈ Fin ∧ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑁 } ⊆ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ) → { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑁 } ∈ Fin )
10 7 8 9 mp2an { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑁 } ∈ Fin
11 3 10 eqeltrdi ( 𝜑 → ( 𝐶𝑁 ) ∈ Fin )