Metamath Proof Explorer

Theorem indfval

Description: Value of the indicator function. (Contributed by Thierry Arnoux, 13-Aug-2017)

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

Proof

Step Hyp Ref Expression
1 indval 
 |-  ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) = ( x e. O |-> if ( x e. A , 1 , 0 ) ) )
2 1 3adant3 
 |-  ( ( O e. V /\ A C_ O /\ X e. O ) -> ( ( _Ind ` O ) ` A ) = ( x e. O |-> if ( x e. A , 1 , 0 ) ) )
3 simpr 
 |-  ( ( ( O e. V /\ A C_ O /\ X e. O ) /\ x = X ) -> x = X )
4 3 eleq1d 
 |-  ( ( ( O e. V /\ A C_ O /\ X e. O ) /\ x = X ) -> ( x e. A <-> X e. A ) )
5 4 ifbid 
 |-  ( ( ( O e. V /\ A C_ O /\ X e. O ) /\ x = X ) -> if ( x e. A , 1 , 0 ) = if ( X e. A , 1 , 0 ) )
6 simp3 
 |-  ( ( O e. V /\ A C_ O /\ X e. O ) -> X e. O )
7 1re 
 |-  1 e. RR
8 0re 
 |-  0 e. RR
9 7 8 ifcli 
 |-  if ( X e. A , 1 , 0 ) e. RR
10 9 a1i 
 |-  ( ( O e. V /\ A C_ O /\ X e. O ) -> if ( X e. A , 1 , 0 ) e. RR )
11 2 5 6 10 fvmptd 
 |-  ( ( O e. V /\ A C_ O /\ X e. O ) -> ( ( ( _Ind ` O ) ` A ) ` X ) = if ( X e. A , 1 , 0 ) )