# Metamath Proof Explorer

## 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 ${class}inftyexpi$
1 vx ${setvar}{x}$
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 ${setvar}{x}$
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 ${wff}inftyexpi=\left({x}\in \left(-\mathrm{\pi },\mathrm{\pi }\right]⟼⟨{x},ℂ⟩\right)$