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∈−ππ∧B∈−ππ→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∈−ππ→1st⁡inftyexpi⁡A=A
4 3 adantr ⊢A∈−ππ∧B∈−ππ→1st⁡inftyexpi⁡A=A
5 4 eqeq1d ⊢A∈−ππ∧B∈−ππ→1st⁡inftyexpi⁡A=1st⁡inftyexpi⁡B↔A=1st⁡inftyexpi⁡B
6 5 biimpd ⊢A∈−ππ∧B∈−ππ→1st⁡inftyexpi⁡A=1st⁡inftyexpi⁡B→A=1st⁡inftyexpi⁡B
7 bj-inftyexpiinv ⊢B∈−ππ→1st⁡inftyexpi⁡B=B
8 7 adantl ⊢A∈−ππ∧B∈−ππ→1st⁡inftyexpi⁡B=B
9 8 eqeq2d ⊢A∈−ππ∧B∈−ππ→A=1st⁡inftyexpi⁡B↔A=B
10 6 9 sylibd ⊢A∈−ππ∧B∈−ππ→1st⁡inftyexpi⁡A=1st⁡inftyexpi⁡B→A=B
11 2 10 syl5 ⊢A∈−ππ∧B∈−ππ→inftyexpi⁡A=inftyexpi⁡B→A=B
12 1 11 impbid2 ⊢A∈−ππ∧B∈−ππ→A=B↔inftyexpi⁡A=inftyexpi⁡B