Metamath Proof Explorer

Theorem ind1

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

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

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( O e. V /\ A C_ O /\ X e. A ) -> A C_ O )
2 simp3 
 |-  ( ( O e. V /\ A C_ O /\ X e. A ) -> X e. A )
3 1 2 sseldd 
 |-  ( ( O e. V /\ A C_ O /\ X e. A ) -> X e. O )
4 indfval 
 |-  ( ( O e. V /\ A C_ O /\ X e. O ) -> ( ( ( _Ind ` O ) ` A ) ` X ) = if ( X e. A , 1 , 0 ) )
5 3 4 syld3an3 
 |-  ( ( O e. V /\ A C_ O /\ X e. A ) -> ( ( ( _Ind ` O ) ` A ) ` X ) = if ( X e. A , 1 , 0 ) )
6 iftrue 
 |-  ( X e. A -> if ( X e. A , 1 , 0 ) = 1 )
7 6 3ad2ant3 
 |-  ( ( O e. V /\ A C_ O /\ X e. A ) -> if ( X e. A , 1 , 0 ) = 1 )
8 5 7 eqtrd 
 |-  ( ( O e. V /\ A C_ O /\ X e. A ) -> ( ( ( _Ind ` O ) ` A ) ` X ) = 1 )