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 = x π π x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cinftyexpi class inftyexpi
1 vx setvar x
2 cpi class π
3 2 cneg class π
4 cioc class .
5 3 2 4 co class π π
6 1 cv setvar x
7 cc class
8 6 7 cop class x
9 1 5 8 cmpt class x π π x
10 0 9 wceq wff inftyexpi = x π π x