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	|- ( A e. ( -u _pi (,] _pi ) -> ( 1st ` ( inftyexpi ` A ) ) = A )

Proof

Step	Hyp	Ref	Expression
1		opeq1	|- ( x = A -> <. x , CC >. = <. A , CC >. )
2		df-bj-inftyexpi	|- inftyexpi = ( x e. ( -u _pi (,] _pi ) |-> <. x , CC >. )
3		opex	|- <. A , CC >. e. _V
4	1 2 3	fvmpt	|- ( A e. ( -u _pi (,] _pi ) -> ( inftyexpi ` A ) = <. A , CC >. )
5	4	fveq2d	|- ( A e. ( -u _pi (,] _pi ) -> ( 1st ` ( inftyexpi ` A ) ) = ( 1st ` <. A , CC >. ) )
6		cnex	|- CC e. _V
7		op1stg	|- ( ( A e. ( -u _pi (,] _pi ) /\ CC e. _V ) -> ( 1st ` <. A , CC >. ) = A )
8	6 7	mpan2	|- ( A e. ( -u _pi (,] _pi ) -> ( 1st ` <. A , CC >. ) = A )
9	5 8	eqtrd	|- ( A e. ( -u _pi (,] _pi ) -> ( 1st ` ( inftyexpi ` A ) ) = A )