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