Theorem bj-inftyexpitaufo

Description: The function inftyexpitau written as a surjection with domain and range. (Contributed by BJ, 4-Feb-2023)

	Ref	Expression
Assertion	bj-inftyexpitaufo	$$⊢{\mathrm{+\infty e}}^{i\tau }:ℝ\underset{onto}{⟶}{ℂ}_{\infty N}$$

Proof

Step	Hyp	Ref	Expression
1		opex	$$⊢⟨{\{}_R\left(1^{st}\left(x\right)\right),\left\{𝑹\right\}⟩\in \mathrm{V}$$
2		df-bj-inftyexpitau	$$⊢{\mathrm{+\infty e}}^{i\tau }=\left(x\in ℝ⟼⟨{\{}_R\left(1^{st}\left(x\right)\right),\left\{𝑹\right\}⟩\right)$$
3	1 2	fnmpti	$$⊢{\mathrm{+\infty e}}^{i\tau }Fnℝ$$
4		dffn4	$$⊢{\mathrm{+\infty e}}^{i\tau }Fnℝ\leftrightarrow {\mathrm{+\infty e}}^{i\tau }:ℝ\underset{onto}{⟶}\mathrm{ran}{\mathrm{+\infty e}}^{i\tau }$$
5	3 4	mpbi	$$⊢{\mathrm{+\infty e}}^{i\tau }:ℝ\underset{onto}{⟶}\mathrm{ran}{\mathrm{+\infty e}}^{i\tau }$$
6		df-bj-ccinftyN	$$⊢{ℂ}_{\infty N}$$
7	6	eqcomi	$$⊢\mathrm{ran}{\mathrm{+\infty e}}^{i\tau }={ℂ}_{\infty N}$$
8		foeq3	$$⊢\mathrm{ran}{\mathrm{+\infty e}}^{i\tau }={ℂ}_{\infty N}\to \left({\mathrm{+\infty e}}^{i\tau }:ℝ\underset{onto}{⟶}\mathrm{ran}{\mathrm{+\infty e}}^{i\tau }\leftrightarrow {\mathrm{+\infty e}}^{i\tau }:ℝ\underset{onto}{⟶}{ℂ}_{\infty N}\right)$$
9	7 8	ax-mp	$$⊢{\mathrm{+\infty e}}^{i\tau }:ℝ\underset{onto}{⟶}\mathrm{ran}{\mathrm{+\infty e}}^{i\tau }\leftrightarrow {\mathrm{+\infty e}}^{i\tau }:ℝ\underset{onto}{⟶}{ℂ}_{\infty N}$$
10	5 9	mpbi	$$⊢{\mathrm{+\infty e}}^{i\tau }:ℝ\underset{onto}{⟶}{ℂ}_{\infty N}$$