Theorem psrelbas

Description: An element of the set of power series is a function on the coefficients. (Contributed by Mario Carneiro, 28-Dec-2014)

	Ref	Expression
Hypotheses	psrbas.s	$$⊢S=I\mathrm{mPwSer}R$$
	psrbas.k	$$⊢K={\mathrm{Base}}_R$$
	psrbas.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	psrbas.b	$$⊢B={\mathrm{Base}}_S$$
	psrelbas.x	$$⊢\phi \to X\in B$$
Assertion	psrelbas	$$⊢\phi \to X:D⟶K$$

Proof

Step	Hyp	Ref	Expression
1		psrbas.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psrbas.k	$$⊢K={\mathrm{Base}}_R$$
3		psrbas.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
4		psrbas.b	$$⊢B={\mathrm{Base}}_S$$
5		psrelbas.x	$$⊢\phi \to X\in B$$
6		reldmpsr	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mPwSer}$$
7	6 1 4	elbasov	$$⊢X\in B\to \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)$$
8	5 7	syl	$$⊢\phi \to \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)$$
9	8	simpld	$$⊢\phi \to I\in \mathrm{V}$$
10	1 2 3 4 9	psrbas	$$⊢\phi \to B=K^D$$
11	5 10	eleqtrd	$$⊢\phi \to X\in \left(K^D\right)$$
12	2	fvexi	$$⊢K\in \mathrm{V}$$
13		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
14	3 13	rabex2	$$⊢D\in \mathrm{V}$$
15	12 14	elmap	$$⊢X\in \left(K^D\right)\leftrightarrow X:D⟶K$$
16	11 15	sylib	$$⊢\phi \to X:D⟶K$$