Metamath Proof Explorer

Theorem bj-inftyexpiinj

Description: Injectivity of the parameterization inftyexpi . Remark: a more conceptual proof would use bj-inftyexpiinv and the fact that a function with a retraction is injective. (Contributed by BJ, 22-Jun-2019)

Ref Expression
Assertion bj-inftyexpiinj 
|- ( ( A e. ( -u _pi (,] _pi ) /\ B e. ( -u _pi (,] _pi ) ) -> ( A = B <-> ( inftyexpi ` A ) = ( inftyexpi ` B ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( A = B -> ( inftyexpi ` A ) = ( inftyexpi ` B ) )
2 fveq2 
 |-  ( ( inftyexpi ` A ) = ( inftyexpi ` B ) -> ( 1st ` ( inftyexpi ` A ) ) = ( 1st ` ( inftyexpi ` B ) ) )
3 bj-inftyexpiinv 
 |-  ( A e. ( -u _pi (,] _pi ) -> ( 1st ` ( inftyexpi ` A ) ) = A )
4 3 adantr 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ B e. ( -u _pi (,] _pi ) ) -> ( 1st ` ( inftyexpi ` A ) ) = A )
5 4 eqeq1d 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ B e. ( -u _pi (,] _pi ) ) -> ( ( 1st ` ( inftyexpi ` A ) ) = ( 1st ` ( inftyexpi ` B ) ) <-> A = ( 1st ` ( inftyexpi ` B ) ) ) )
6 5 biimpd 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ B e. ( -u _pi (,] _pi ) ) -> ( ( 1st ` ( inftyexpi ` A ) ) = ( 1st ` ( inftyexpi ` B ) ) -> A = ( 1st ` ( inftyexpi ` B ) ) ) )
7 bj-inftyexpiinv 
 |-  ( B e. ( -u _pi (,] _pi ) -> ( 1st ` ( inftyexpi ` B ) ) = B )
8 7 adantl 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ B e. ( -u _pi (,] _pi ) ) -> ( 1st ` ( inftyexpi ` B ) ) = B )
9 8 eqeq2d 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ B e. ( -u _pi (,] _pi ) ) -> ( A = ( 1st ` ( inftyexpi ` B ) ) <-> A = B ) )
10 6 9 sylibd 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ B e. ( -u _pi (,] _pi ) ) -> ( ( 1st ` ( inftyexpi ` A ) ) = ( 1st ` ( inftyexpi ` B ) ) -> A = B ) )
11 2 10 syl5 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ B e. ( -u _pi (,] _pi ) ) -> ( ( inftyexpi ` A ) = ( inftyexpi ` B ) -> A = B ) )
12 1 11 impbid2 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ B e. ( -u _pi (,] _pi ) ) -> ( A = B <-> ( inftyexpi ` A ) = ( inftyexpi ` B ) ) )