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 | ||
Assertion | pw2f1o2val |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pw2f1o2.f | ||
2 | cnvexg | ||
3 | imaexg | ||
4 | 2 3 | syl | |
5 | cnveq | ||
6 | 5 | imaeq1d | |
7 | 6 1 | fvmptg | |
8 | 4 7 | mpdan |