etransclem12

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

	Ref	Expression
Hypotheses	etransclem12.1	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
	etransclem12.2	$⊢ φ \to N \in ℕ_{0}$
Assertion	etransclem12	$⊢ φ \to C (N) = \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}$

Step	Hyp	Ref	Expression
1		etransclem12.1	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
2		etransclem12.2	$⊢ φ \to N \in ℕ_{0}$
3		oveq2	$⊢ n = N \to (0 \dots n) = (0 \dots N)$
4	3	oveq1d	$⊢ n = N \to {(0 \dots n)}^{(0 \dots M)} = {(0 \dots N)}^{(0 \dots M)}$
5		eqeq2	$⊢ n = N \to (\sum_{j = 0}^{M} c (j) = n \leftrightarrow \sum_{j = 0}^{M} c (j) = N)$
6	4 5	rabeqbidv	$⊢ n = N \to \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\} = \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}$
7		ovex	$⊢ {(0 \dots N)}^{(0 \dots M)} \in V$
8	7	rabex	$⊢ \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \in V$
9	8	a1i	$⊢ φ \to \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \in V$
10	1 6 2 9	fvmptd3	$⊢ φ \to C (N) = \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}$

Metamath Proof Explorer