Metamath Proof Explorer

Theorem indf1o

Description: The bijection between a power set and the set of indicator functions. (Contributed by Thierry Arnoux, 14-Aug-2017)

Ref Expression
Assertion indf1o 
|- ( O e. V -> ( _Ind ` O ) : ~P O -1-1-onto-> ( { 0 , 1 } ^m O ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( O e. V -> O e. V )
2 0red 
 |-  ( O e. V -> 0 e. RR )
3 1red 
 |-  ( O e. V -> 1 e. RR )
4 0ne1 
 |-  0 =/= 1
5 4 a1i 
 |-  ( O e. V -> 0 =/= 1 )
6 eqid 
 |-  ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) = ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) )
7 1 2 3 5 6 pw2f1o 
 |-  ( O e. V -> ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) : ~P O -1-1-onto-> ( { 0 , 1 } ^m O ) )
8 indv 
 |-  ( O e. V -> ( _Ind ` O ) = ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) )
9 8 f1oeq1d 
 |-  ( O e. V -> ( ( _Ind ` O ) : ~P O -1-1-onto-> ( { 0 , 1 } ^m O ) <-> ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) : ~P O -1-1-onto-> ( { 0 , 1 } ^m O ) ) )
10 7 9 mpbird 
 |-  ( O e. V -> ( _Ind ` O ) : ~P O -1-1-onto-> ( { 0 , 1 } ^m O ) )