Definition df-ind

Description: Define the indicator function generator. (Contributed by Thierry Arnoux, 20-Jan-2017)

	Ref	Expression
Assertion	df-ind	|- _Ind = ( o e. _V |-> ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cind	|- _Ind
1		vo	|- o
2		cvv	|- _V
3		va	|- a
4	1	cv	|- o
5	4	cpw	|- ~P o
6		vx	|- x
7	6	cv	|- x
8	3	cv	|- a
9	7 8	wcel	|- x e. a
10		c1	|- 1
11		cc0	|- 0
12	9 10 11	cif	|- if ( x e. a , 1 , 0 )
13	6 4 12	cmpt	|- ( x e. o |-> if ( x e. a , 1 , 0 ) )
14	3 5 13	cmpt	|- ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) )
15	1 2 14	cmpt	|- ( o e. _V |-> ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) ) )
16	0 15	wceq	|- _Ind = ( o e. _V |-> ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) ) )