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

Metamath Proof Explorer

Theorem ind0

Description: Value of the indicator function where it is 0 . (Contributed by Thierry Arnoux, 14-Aug-2017)

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

Proof

Step Hyp Ref Expression
1 eldifi 
 |-  ( X e. ( O \ A ) -> X e. O )
2 indfval 
 |-  ( ( O e. V /\ A C_ O /\ X e. O ) -> ( ( ( _Ind ` O ) ` A ) ` X ) = if ( X e. A , 1 , 0 ) )
3 1 2 syl3an3 
 |-  ( ( O e. V /\ A C_ O /\ X e. ( O \ A ) ) -> ( ( ( _Ind ` O ) ` A ) ` X ) = if ( X e. A , 1 , 0 ) )
4 eldifn 
 |-  ( X e. ( O \ A ) -> -. X e. A )
5 4 3ad2ant3 
 |-  ( ( O e. V /\ A C_ O /\ X e. ( O \ A ) ) -> -. X e. A )
6 5 iffalsed 
 |-  ( ( O e. V /\ A C_ O /\ X e. ( O \ A ) ) -> if ( X e. A , 1 , 0 ) = 0 )
7 3 6 eqtrd 
 |-  ( ( O e. V /\ A C_ O /\ X e. ( O \ A ) ) -> ( ( ( _Ind ` O ) ` A ) ` X ) = 0 )