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

Metamath Proof Explorer

Theorem pw2f1o2val2

Description: Membership in a mapped set under 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 pw2f1o2val2 
|- ( ( X e. ( 2o ^m A ) /\ Y e. A ) -> ( Y e. ( F ` X ) <-> ( X ` Y ) = 1o ) )

Proof

Step Hyp Ref Expression
1 pw2f1o2.f 
 |-  F = ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) )
2 1 pw2f1o2val 
 |-  ( X e. ( 2o ^m A ) -> ( F ` X ) = ( `' X " { 1o } ) )
3 2 eleq2d 
 |-  ( X e. ( 2o ^m A ) -> ( Y e. ( F ` X ) <-> Y e. ( `' X " { 1o } ) ) )
4 3 adantr 
 |-  ( ( X e. ( 2o ^m A ) /\ Y e. A ) -> ( Y e. ( F ` X ) <-> Y e. ( `' X " { 1o } ) ) )
5 elmapi 
 |-  ( X e. ( 2o ^m A ) -> X : A --> 2o )
6 ffn 
 |-  ( X : A --> 2o -> X Fn A )
7 fniniseg 
 |-  ( X Fn A -> ( Y e. ( `' X " { 1o } ) <-> ( Y e. A /\ ( X ` Y ) = 1o ) ) )
8 5 6 7 3syl 
 |-  ( X e. ( 2o ^m A ) -> ( Y e. ( `' X " { 1o } ) <-> ( Y e. A /\ ( X ` Y ) = 1o ) ) )
9 8 baibd 
 |-  ( ( X e. ( 2o ^m A ) /\ Y e. A ) -> ( Y e. ( `' X " { 1o } ) <-> ( X ` Y ) = 1o ) )
10 4 9 bitrd 
 |-  ( ( X e. ( 2o ^m A ) /\ Y e. A ) -> ( Y e. ( F ` X ) <-> ( X ` Y ) = 1o ) )