Theorem bj-inftyexpiinv

Description: Utility theorem for the inverse of inftyexpi . (Contributed by BJ, 22-Jun-2019) This utility theorem is irrelevant and should generally not be used. (New usage is discouraged.)

	Ref	Expression
Assertion	bj-inftyexpiinv	⊢ ( 𝐴 ∈ ( - π (,] π ) → ( 1st ‘ ( +∞ei ‘ 𝐴 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		opeq1	⊢ ( 𝑥 = 𝐴 → ⟨ 𝑥 , ℂ ⟩ = ⟨ 𝐴 , ℂ ⟩ )
2		df-bj-inftyexpi	⊢ +∞ei = ( 𝑥 ∈ ( - π (,] π ) ↦ ⟨ 𝑥 , ℂ ⟩ )
3		opex	⊢ ⟨ 𝐴 , ℂ ⟩ ∈ V
4	1 2 3	fvmpt	⊢ ( 𝐴 ∈ ( - π (,] π ) → ( +∞ei ‘ 𝐴 ) = ⟨ 𝐴 , ℂ ⟩ )
5	4	fveq2d	⊢ ( 𝐴 ∈ ( - π (,] π ) → ( 1st ‘ ( +∞ei ‘ 𝐴 ) ) = ( 1st ‘ ⟨ 𝐴 , ℂ ⟩ ) )
6		cnex	⊢ ℂ ∈ V
7		op1stg	⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ ℂ ∈ V ) → ( 1st ‘ ⟨ 𝐴 , ℂ ⟩ ) = 𝐴 )
8	6 7	mpan2	⊢ ( 𝐴 ∈ ( - π (,] π ) → ( 1st ‘ ⟨ 𝐴 , ℂ ⟩ ) = 𝐴 )
9	5 8	eqtrd	⊢ ( 𝐴 ∈ ( - π (,] π ) → ( 1st ‘ ( +∞ei ‘ 𝐴 ) ) = 𝐴 )