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 ) |