This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem indf

Description: An indicator function as a function with domain and codomain. (Contributed by Thierry Arnoux, 13-Aug-2017)

Ref Expression
Assertion indf 
|- ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) : O --> { 0 , 1 } )

Proof

Step Hyp Ref Expression
1 indval 
 |-  ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) = ( x e. O |-> if ( x e. A , 1 , 0 ) ) )
2 1re 
 |-  1 e. RR
3 0re 
 |-  0 e. RR
4 ifpr 
 |-  ( ( 1 e. RR /\ 0 e. RR ) -> if ( x e. A , 1 , 0 ) e. { 1 , 0 } )
5 2 3 4 mp2an 
 |-  if ( x e. A , 1 , 0 ) e. { 1 , 0 }
6 prcom 
 |-  { 1 , 0 } = { 0 , 1 }
7 5 6 eleqtri 
 |-  if ( x e. A , 1 , 0 ) e. { 0 , 1 }
8 7 a1i 
 |-  ( ( ( O e. V /\ A C_ O ) /\ x e. O ) -> if ( x e. A , 1 , 0 ) e. { 0 , 1 } )
9 1 8 fmpt3d 
 |-  ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) : O --> { 0 , 1 } )