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 )