Theorem psrelbasfun

Description: An element of the set of power series is a function. (Contributed by AV, 17-Jul-2019)

	Ref	Expression
Hypotheses	psrelbasfun.s	$$⊢S=I\mathrm{mPwSer}R$$
	psrelbasfun.b	$$⊢B={\mathrm{Base}}_S$$
Assertion	psrelbasfun	$$⊢X\in B\to \mathrm{Fun}X$$

Proof

Step	Hyp	Ref	Expression
1		psrelbasfun.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psrelbasfun.b	$$⊢B={\mathrm{Base}}_S$$
3		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
4		eqid	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
5		id	$$⊢X\in B\to X\in B$$
6	1 3 4 2 5	psrelbas	$$⊢X\in B\to X:\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
7	6	ffund	$$⊢X\in B\to \mathrm{Fun}X$$