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