Theorem bj-elccinfty

Description: A lemma for infinite extended complex numbers. (Contributed by BJ, 27-Jun-2019)

	Ref	Expression
Assertion	bj-elccinfty	⊢ ( 𝐴 ∈ ( - π (,] π ) → ( +∞ei ‘ 𝐴 ) ∈ ℂ∞ )

Proof

Step	Hyp	Ref	Expression
1		df-bj-inftyexpi	⊢ +∞ei = ( 𝑥 ∈ ( - π (,] π ) ↦ ⟨ 𝑥 , ℂ ⟩ )
2	1	funmpt2	⊢ Fun +∞ei
3	2	jctl	⊢ ( 𝐴 ∈ dom +∞ei → ( Fun +∞ei ∧ 𝐴 ∈ dom +∞ei ) )
4		opex	⊢ ⟨ 𝑥 , ℂ ⟩ ∈ V
5	4 1	dmmpti	⊢ dom +∞ei = ( - π (,] π )
6	5	eqcomi	⊢ ( - π (,] π ) = dom +∞ei
7	3 6	eleq2s	⊢ ( 𝐴 ∈ ( - π (,] π ) → ( Fun +∞ei ∧ 𝐴 ∈ dom +∞ei ) )
8		fvelrn	⊢ ( ( Fun +∞ei ∧ 𝐴 ∈ dom +∞ei ) → ( +∞ei ‘ 𝐴 ) ∈ ran +∞ei )
9		df-bj-ccinfty	⊢ ℂ∞ = ran +∞ei
10	9	eqcomi	⊢ ran +∞ei = ℂ∞
11	10	eleq2i	⊢ ( ( +∞ei ‘ 𝐴 ) ∈ ran +∞ei ↔ ( +∞ei ‘ 𝐴 ) ∈ ℂ∞ )
12	11	biimpi	⊢ ( ( +∞ei ‘ 𝐴 ) ∈ ran +∞ei → ( +∞ei ‘ 𝐴 ) ∈ ℂ∞ )
13	7 8 12	3syl	⊢ ( 𝐴 ∈ ( - π (,] π ) → ( +∞ei ‘ 𝐴 ) ∈ ℂ∞ )