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	⊢ +∞eiτ : ℝ –onto→ ℂ∞N

Proof

Step	Hyp	Ref	Expression
1		opex	⊢ ⟨ ( {R ‘ ( 1st ‘ 𝑥 ) ) , { R } ⟩ ∈ V
2		df-bj-inftyexpitau	⊢ +∞eiτ = ( 𝑥 ∈ ℝ ↦ ⟨ ( {R ‘ ( 1st ‘ 𝑥 ) ) , { R } ⟩ )
3	1 2	fnmpti	⊢ +∞eiτ Fn ℝ
4		dffn4	⊢ ( +∞eiτ Fn ℝ ↔ +∞eiτ : ℝ –onto→ ran +∞eiτ )
5	3 4	mpbi	⊢ +∞eiτ : ℝ –onto→ ran +∞eiτ
6		df-bj-ccinftyN	⊢ ℂ∞N = ran +∞eiτ
7	6	eqcomi	⊢ ran +∞eiτ = ℂ∞N
8		foeq3	⊢ ( ran +∞eiτ = ℂ∞N → ( +∞eiτ : ℝ –onto→ ran +∞eiτ ↔ +∞eiτ : ℝ –onto→ ℂ∞N ) )
9	7 8	ax-mp	⊢ ( +∞eiτ : ℝ –onto→ ran +∞eiτ ↔ +∞eiτ : ℝ –onto→ ℂ∞N )
10	5 9	mpbi	⊢ +∞eiτ : ℝ –onto→ ℂ∞N