This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. ( 2o ^m A ) |-> ( `' x " { 1o } ) )
Assertion pw2f1o2val 
|- ( X e. ( 2o ^m A ) -> ( F ` X ) = ( `' X " { 1o } ) )

Proof

Step Hyp Ref Expression
1 pw2f1o2.f 
 |-  F = ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) )
2 cnvexg 
 |-  ( X e. ( 2o ^m A ) -> `' X e. _V )
3 imaexg 
 |-  ( `' X e. _V -> ( `' X " { 1o } ) e. _V )
4 2 3 syl 
 |-  ( X e. ( 2o ^m A ) -> ( `' X " { 1o } ) e. _V )
5 cnveq 
 |-  ( x = X -> `' x = `' X )
6 5 imaeq1d 
 |-  ( x = X -> ( `' x " { 1o } ) = ( `' X " { 1o } ) )
7 6 1 fvmptg 
 |-  ( ( X e. ( 2o ^m A ) /\ ( `' X " { 1o } ) e. _V ) -> ( F ` X ) = ( `' X " { 1o } ) )
8 4 7 mpdan 
 |-  ( X e. ( 2o ^m A ) -> ( F ` X ) = ( `' X " { 1o } ) )