Definition df-ind

Description: Define the indicator function generator. It generates an indicator function ( ( _IndO )A ) for a given domain O and a given subset A of the domain, see indval . In contrast to the definitions and notations in Wikipedia and Lang2 p. 3, the domain and the subset are always mentioned explicitly. (Contributed by Thierry Arnoux, 20-Jan-2017)

	Ref	Expression
Assertion	df-ind	$$⊢𝟙=\left(o\in \mathrm{V}⟼\left(a\in 𝒫o⟼\left(x\in o⟼if\left(x\in a,1,0\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cind	$$class𝟙$$
1		vo	$$setvaro$$
2		cvv	$$class\mathrm{V}$$
3		va	$$setvara$$
4	1	cv	$$setvaro$$
5	4	cpw	$$class𝒫o$$
6		vx	$$setvarx$$
7	6	cv	$$setvarx$$
8	3	cv	$$setvara$$
9	7 8	wcel	$$wffx\in a$$
10		c1	$$class1$$
11		cc0	$$class0$$
12	9 10 11	cif	$$classif\left(x\in a,1,0\right)$$
13	6 4 12	cmpt	$$class\left(x\in o⟼if\left(x\in a,1,0\right)\right)$$
14	3 5 13	cmpt	$$class\left(a\in 𝒫o⟼\left(x\in o⟼if\left(x\in a,1,0\right)\right)\right)$$
15	1 2 14	cmpt	$$class\left(o\in \mathrm{V}⟼\left(a\in 𝒫o⟼\left(x\in o⟼if\left(x\in a,1,0\right)\right)\right)\right)$$
16	0 15	wceq	$$wff𝟙=\left(o\in \mathrm{V}⟼\left(a\in 𝒫o⟼\left(x\in o⟼if\left(x\in a,1,0\right)\right)\right)\right)$$