Definition df-bj-inftyexpi 38221

Description: Definition of the auxiliary function +∞eⁱ parameterizing the circle at infinity ℂ_∞ in ℂ̅. We use coupling with ℂ to simplify the proof of bj-ccinftydisj 38227. It could seem more natural to define +∞eⁱ on all of ℝ, but we want to use only basic functions in the definition of ℂ̅. TODO: transition to df-bj-inftyexpitau 38213 instead. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.)

Assertion

Ref	Expression
df-bj-inftyexpi	⊢ +∞ei = (𝑥 ∈ ( -π(,]π) ↦ ⟨𝑥, ℂ⟩)

Detailed syntax breakdown of Definition df-bj-inftyexpi

Step	Hyp	Ref	Expression
1		cinftyexpi 38220	. 2 class +∞ei
2		vx	. . 3 setvar 𝑥
3		cpi 16237	. . . . 5 class π
4	3	cneg 11545	. . . 4 class -π
5		cioc 13480	. . . 4 class (,]
6	4, 3, 5	co 7420	. . 3 class ( -π(,]π)
7	2	cv 1568	. . . 4 class 𝑥
8		cc 11201	. . . 4 class ℂ
9	7, 8	cop 4834	. . 3 class ⟨𝑥, ℂ⟩
10	2, 6, 9	cmpt 5185	. 2 class (𝑥 ∈ ( -π(,]π) ↦ ⟨𝑥, ℂ⟩)
11	1, 10	wceq 1569	1 wff +∞ei = (𝑥 ∈ ( -π(,]π) ↦ ⟨𝑥, ℂ⟩)

This definition is used by:  bj-inftyexpiinv  38222  bj-inftyexpidisj  38224  bj-ccinftydisj  38227  bj-elccinfty  38228  bj-minftyccb  38239