Theorem indval

Description: Value of the indicator function generator for a set A and a domain O . (Contributed by Thierry Arnoux, 2-Feb-2017)

	Ref	Expression
Assertion	indval	|- ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) = ( x e. O |-> if ( x e. A , 1 , 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		indv	|- ( O e. V -> ( _Ind ` O ) = ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) )
2	1	adantr	|- ( ( O e. V /\ A C_ O ) -> ( _Ind ` O ) = ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) )
3		eleq2	|- ( a = A -> ( x e. a <-> x e. A ) )
4	3	ifbid	|- ( a = A -> if ( x e. a , 1 , 0 ) = if ( x e. A , 1 , 0 ) )
5	4	mpteq2dv	|- ( a = A -> ( x e. O |-> if ( x e. a , 1 , 0 ) ) = ( x e. O |-> if ( x e. A , 1 , 0 ) ) )
6	5	adantl	|- ( ( ( O e. V /\ A C_ O ) /\ a = A ) -> ( x e. O |-> if ( x e. a , 1 , 0 ) ) = ( x e. O |-> if ( x e. A , 1 , 0 ) ) )
7		ssexg	|- ( ( A C_ O /\ O e. V ) -> A e. _V )
8	7	ancoms	|- ( ( O e. V /\ A C_ O ) -> A e. _V )
9		simpr	|- ( ( O e. V /\ A C_ O ) -> A C_ O )
10	8 9	elpwd	|- ( ( O e. V /\ A C_ O ) -> A e. ~P O )
11		mptexg	|- ( O e. V -> ( x e. O |-> if ( x e. A , 1 , 0 ) ) e. _V )
12	11	adantr	|- ( ( O e. V /\ A C_ O ) -> ( x e. O |-> if ( x e. A , 1 , 0 ) ) e. _V )
13	2 6 10 12	fvmptd	|- ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) = ( x e. O |-> if ( x e. A , 1 , 0 ) ) )