Definition df-bj-inftyexpi 33094

Description: Definition of the auxiliary function inftyexpi parameterizing the circle at infinity CCinfty in CCbar. We use coupling with CC to simplify the proof of bj-ccinftydisj 33100. It could seem more natural to define inftyexpi on all of RR using prcpal but we want to use only basic functions in the definition of CCbar. (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	|- inftyexpi = ( x e. ( -u pi (,] pi ) |-> <. x , CC >. )

Detailed syntax breakdown of Definition df-bj-inftyexpi

Step	Hyp	Ref	Expression
1		cinftyexpi 33093	. 2 class inftyexpi
2		vx	. . 3 setvar x
3		cpi 14797	. . . . 5 class pi
4	3	cneg 10267	. . . 4 class -u pi
5		cioc 12176	. . . 4 class (,]
6	4, 3, 5	co 6650	. . 3 class ( -u pi (,] pi )
7	2	cv 1482	. . . 4 class x
8		cc 9934	. . . 4 class CC
9	7, 8	cop 4183	. . 3 class <. x , CC >.
10	2, 6, 9	cmpt 4729	. 2 class ( x e. ( -u pi (,] pi ) |-> <. x , CC >. )
11	1, 10	wceq 1483	1 wff inftyexpi = ( x e. ( -u pi (,] pi ) |-> <. x , CC >. )

This definition is referenced by:  bj-inftyexpiinv  33095  bj-inftyexpidisj  33097  bj-ccinftydisj  33100  bj-elccinfty  33101  bj-minftyccb  33112