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

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

Metamath Proof Explorer