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 ${⊢}{C}=\left({n}\in {ℕ}_{0}⟼\left\{{c}\in \left({\left(0\dots {n}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={n}\right\}\right)$
etransclem16.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
Assertion etransclem16 ${⊢}{\phi }\to {C}\left({N}\right)\in \mathrm{Fin}$

Proof

Step Hyp Ref Expression
1 etransclem16.c ${⊢}{C}=\left({n}\in {ℕ}_{0}⟼\left\{{c}\in \left({\left(0\dots {n}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={n}\right\}\right)$
2 etransclem16.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
3 1 2 etransclem12 ${⊢}{\phi }\to {C}\left({N}\right)=\left\{{c}\in \left({\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={N}\right\}$
4 fzfi ${⊢}\left(0\dots {N}\right)\in \mathrm{Fin}$
5 fzfi ${⊢}\left(0\dots {M}\right)\in \mathrm{Fin}$
6 mapfi ${⊢}\left(\left(0\dots {N}\right)\in \mathrm{Fin}\wedge \left(0\dots {M}\right)\in \mathrm{Fin}\right)\to {\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\in \mathrm{Fin}$
7 4 5 6 mp2an ${⊢}{\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\in \mathrm{Fin}$
8 ssrab2 ${⊢}\left\{{c}\in \left({\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={N}\right\}\subseteq {\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}$
9 ssfi ${⊢}\left({\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\in \mathrm{Fin}\wedge \left\{{c}\in \left({\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={N}\right\}\subseteq {\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\right)\to \left\{{c}\in \left({\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={N}\right\}\in \mathrm{Fin}$
10 7 8 9 mp2an ${⊢}\left\{{c}\in \left({\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={N}\right\}\in \mathrm{Fin}$
11 3 10 eqeltrdi ${⊢}{\phi }\to {C}\left({N}\right)\in \mathrm{Fin}$