Definition df-bj-inftyexpi

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 . It could seem more natural to define inftyexpi on all of RR , but we want to use only basic functions in the definition of CCbar . TODO: transition to df-bj-inftyexpitau instead. (Contributed by BJ, 22-Jun-2019) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.)

	Ref	Expression
Assertion	df-bj-inftyexpi	$$⊢inftyexpi=\left(x\in \left(-\mathrm{\pi },\mathrm{\pi }\right]⟼⟨x,ℂ⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinftyexpi	$$classinftyexpi$$
1		vx	$$setvarx$$
2		cpi	$$class\mathrm{\pi }$$
3	2	cneg	$$class\left(-\mathrm{\pi }\right)$$
4		cioc	$$class\left(.\right]$$
5	3 2 4	co	$$class\left(-\mathrm{\pi },\mathrm{\pi }\right]$$
6	1	cv	$$setvarx$$
7		cc	$$classℂ$$
8	6 7	cop	$$class⟨x,ℂ⟩$$
9	1 5 8	cmpt	$$class\left(x\in \left(-\mathrm{\pi },\mathrm{\pi }\right]⟼⟨x,ℂ⟩\right)$$
10	0 9	wceq	$$wffinftyexpi=\left(x\in \left(-\mathrm{\pi },\mathrm{\pi }\right]⟼⟨x,ℂ⟩\right)$$