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 )