Metamath Proof Explorer


Theorem pw2f1o2val

Description: Function value of the pw2f1o2 bijection. (Contributed by Stefan O'Rear, 18-Jan-2015) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypothesis pw2f1o2.f F = x 2 𝑜 A x -1 1 𝑜
Assertion pw2f1o2val X 2 𝑜 A F X = X -1 1 𝑜

Proof

Step Hyp Ref Expression
1 pw2f1o2.f F = x 2 𝑜 A x -1 1 𝑜
2 cnvexg X 2 𝑜 A X -1 V
3 imaexg X -1 V X -1 1 𝑜 V
4 2 3 syl X 2 𝑜 A X -1 1 𝑜 V
5 cnveq x = X x -1 = X -1
6 5 imaeq1d x = X x -1 1 𝑜 = X -1 1 𝑜
7 6 1 fvmptg X 2 𝑜 A X -1 1 𝑜 V F X = X -1 1 𝑜
8 4 7 mpdan X 2 𝑜 A F X = X -1 1 𝑜