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 )