Metamath Proof Explorer

Theorem indv

Description: Value of the indicator function generator with domain O . (Contributed by Thierry Arnoux, 23-Aug-2017)

Ref Expression
Assertion indv 
|- ( O e. V -> ( _Ind ` O ) = ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 df-ind 
 |-  _Ind = ( o e. _V |-> ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) ) )
2 pweq 
 |-  ( o = O -> ~P o = ~P O )
3 mpteq1 
 |-  ( o = O -> ( x e. o |-> if ( x e. a , 1 , 0 ) ) = ( x e. O |-> if ( x e. a , 1 , 0 ) ) )
4 2 3 mpteq12dv 
 |-  ( o = O -> ( 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 ) ) ) )
5 elex 
 |-  ( O e. V -> O e. _V )
6 pwexg 
 |-  ( O e. _V -> ~P O e. _V )
7 mptexg 
 |-  ( ~P O e. _V -> ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) e. _V )
8 5 6 7 3syl 
 |-  ( O e. V -> ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) e. _V )
9 1 4 5 8 fvmptd3 
 |-  ( O e. V -> ( _Ind ` O ) = ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) )