Theorem breprexplemb

Description: Lemma for breprexp (closure). (Contributed by Thierry Arnoux, 7-Dec-2021)

	Ref	Expression
Hypotheses	breprexp.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	breprexp.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
	breprexp.z	$$⊢\phi \to Z\in ℂ$$
	breprexp.h	$$⊢\phi \to L:\left(0..^S\right)⟶{ℂ}^{\mathbb{N}}$$
	breprexplemb.x	$$⊢\phi \to X\in \left(0..^S\right)$$
	breprexplemb.y	$$⊢\phi \to Y\in \mathbb{N}$$
Assertion	breprexplemb	$$⊢\phi \to L\left(X\right)\left(Y\right)\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		breprexp.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
2		breprexp.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
3		breprexp.z	$$⊢\phi \to Z\in ℂ$$
4		breprexp.h	$$⊢\phi \to L:\left(0..^S\right)⟶{ℂ}^{\mathbb{N}}$$
5		breprexplemb.x	$$⊢\phi \to X\in \left(0..^S\right)$$
6		breprexplemb.y	$$⊢\phi \to Y\in \mathbb{N}$$
7	4 5	ffvelrnd	$$⊢\phi \to L\left(X\right)\in \left({ℂ}^{\mathbb{N}}\right)$$
8		cnex	$$⊢ℂ\in \mathrm{V}$$
9		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
10	8 9	elmap	$$⊢L\left(X\right)\in \left({ℂ}^{\mathbb{N}}\right)\leftrightarrow L\left(X\right):\mathbb{N}⟶ℂ$$
11	7 10	sylib	$$⊢\phi \to L\left(X\right):\mathbb{N}⟶ℂ$$
12	11 6	ffvelrnd	$$⊢\phi \to L\left(X\right)\left(Y\right)\in ℂ$$