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 \in (- π, π] ⟼ ⟨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 \in (- π, π] ⟼ ⟨x, ℂ⟩)$
10	0 9	wceq	$wff inftyexpi = (x \in (- π, π] ⟼ ⟨x, ℂ⟩)$