Definition df-bj-inftyexpitau

Description: Definition of the auxiliary function inftyexpitau parameterizing the circle at infinity CCinfty in CCbar . We use coupling with { R. } to simplify the proof of bj-inftyexpitaudisj . (Contributed by BJ, 22-Jan-2023) The precise definition is irrelevant and should generally not be used. TODO: prove only the necessary lemmas to prove |- ( A e. RR /\ B e. RR ) -> ( ( inftyexpitauA ) = ( inftyexpitauB ) <-> ( A - B ) e. ZZ ) ) . (New usage is discouraged.)

	Ref	Expression
Assertion	df-bj-inftyexpitau	⊢ +∞eiτ = ( 𝑥 ∈ ℝ ↦ ⟨ ( {R ‘ ( 1st ‘ 𝑥 ) ) , { R } ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinftyexpitau	⊢ +∞eiτ
1		vx	⊢ 𝑥
2		cr	⊢ ℝ
3		cfractemp	⊢ {R
4		c1st	⊢ 1st
5	1	cv	⊢ 𝑥
6	5 4	cfv	⊢ ( 1st ‘ 𝑥 )
7	6 3	cfv	⊢ ( {R ‘ ( 1st ‘ 𝑥 ) )
8		cnr	⊢ R
9	8	csn	⊢ { R }
10	7 9	cop	⊢ ⟨ ( {R ‘ ( 1st ‘ 𝑥 ) ) , { R } ⟩
11	1 2 10	cmpt	⊢ ( 𝑥 ∈ ℝ ↦ ⟨ ( {R ‘ ( 1st ‘ 𝑥 ) ) , { R } ⟩ )
12	0 11	wceq	⊢ +∞eiτ = ( 𝑥 ∈ ℝ ↦ ⟨ ( {R ‘ ( 1st ‘ 𝑥 ) ) , { R } ⟩ )