Metamath Proof Explorer

Theorem ind1a

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

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

Proof

Step Hyp Ref Expression
1 indfval 
 |-  ( ( O e. V /\ A C_ O /\ X e. O ) -> ( ( ( _Ind ` O ) ` A ) ` X ) = if ( X e. A , 1 , 0 ) )
2 1 eqeq1d 
 |-  ( ( O e. V /\ A C_ O /\ X e. O ) -> ( ( ( ( _Ind ` O ) ` A ) ` X ) = 1 <-> if ( X e. A , 1 , 0 ) = 1 ) )
3 eqid 
 |-  1 = 1
4 3 biantru 
 |-  ( X e. A <-> ( X e. A /\ 1 = 1 ) )
5 ax-1ne0 
 |-  1 =/= 0
6 5 neii 
 |-  -. 1 = 0
7 6 biorfri 
 |-  ( ( X e. A /\ 1 = 1 ) <-> ( ( X e. A /\ 1 = 1 ) \/ 1 = 0 ) )
8 6 bianfi 
 |-  ( 1 = 0 <-> ( -. X e. A /\ 1 = 0 ) )
9 8 orbi2i 
 |-  ( ( ( X e. A /\ 1 = 1 ) \/ 1 = 0 ) <-> ( ( X e. A /\ 1 = 1 ) \/ ( -. X e. A /\ 1 = 0 ) ) )
10 4 7 9 3bitri 
 |-  ( X e. A <-> ( ( X e. A /\ 1 = 1 ) \/ ( -. X e. A /\ 1 = 0 ) ) )
11 eqif 
 |-  ( 1 = if ( X e. A , 1 , 0 ) <-> ( ( X e. A /\ 1 = 1 ) \/ ( -. X e. A /\ 1 = 0 ) ) )
12 eqcom 
 |-  ( 1 = if ( X e. A , 1 , 0 ) <-> if ( X e. A , 1 , 0 ) = 1 )
13 10 11 12 3bitr2ri 
 |-  ( if ( X e. A , 1 , 0 ) = 1 <-> X e. A )
14 2 13 bitrdi 
 |-  ( ( O e. V /\ A C_ O /\ X e. O ) -> ( ( ( ( _Ind ` O ) ` A ) ` X ) = 1 <-> X e. A ) )