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

Metamath Proof Explorer

Theorem indval

Description: Value of the indicator function generator for a set A and a domain O . (Contributed by Thierry Arnoux, 2-Feb-2017)

Ref Expression
Assertion indval 
|- ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) = ( x e. O |-> if ( x e. A , 1 , 0 ) ) )

Proof

Step Hyp Ref Expression
1 indv 
 |-  ( O e. V -> ( _Ind ` O ) = ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) )
2 1 adantr 
 |-  ( ( O e. V /\ A C_ O ) -> ( _Ind ` O ) = ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) )
3 eleq2 
 |-  ( a = A -> ( x e. a <-> x e. A ) )
4 3 ifbid 
 |-  ( a = A -> if ( x e. a , 1 , 0 ) = if ( x e. A , 1 , 0 ) )
5 4 mpteq2dv 
 |-  ( a = A -> ( x e. O |-> if ( x e. a , 1 , 0 ) ) = ( x e. O |-> if ( x e. A , 1 , 0 ) ) )
6 5 adantl 
 |-  ( ( ( O e. V /\ A C_ O ) /\ a = A ) -> ( x e. O |-> if ( x e. a , 1 , 0 ) ) = ( x e. O |-> if ( x e. A , 1 , 0 ) ) )
7 ssexg 
 |-  ( ( A C_ O /\ O e. V ) -> A e. _V )
8 7 ancoms 
 |-  ( ( O e. V /\ A C_ O ) -> A e. _V )
9 simpr 
 |-  ( ( O e. V /\ A C_ O ) -> A C_ O )
10 8 9 elpwd 
 |-  ( ( O e. V /\ A C_ O ) -> A e. ~P O )
11 mptexg 
 |-  ( O e. V -> ( x e. O |-> if ( x e. A , 1 , 0 ) ) e. _V )
12 11 adantr 
 |-  ( ( O e. V /\ A C_ O ) -> ( x e. O |-> if ( x e. A , 1 , 0 ) ) e. _V )
13 2 6 10 12 fvmptd 
 |-  ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) = ( x e. O |-> if ( x e. A , 1 , 0 ) ) )