Definition df-ind

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

	Ref	Expression
Assertion	df-ind	⊢ 𝟭 = ( 𝑜 ∈ V ↦ ( 𝑎 ∈ 𝒫 𝑜 ↦ ( 𝑥 ∈ 𝑜 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cind	⊢ 𝟭
1		vo	⊢ 𝑜
2		cvv	⊢ V
3		va	⊢ 𝑎
4	1	cv	⊢ 𝑜
5	4	cpw	⊢ 𝒫 𝑜
6		vx	⊢ 𝑥
7	6	cv	⊢ 𝑥
8	3	cv	⊢ 𝑎
9	7 8	wcel	⊢ 𝑥 ∈ 𝑎
10		c1	⊢ 1
11		cc0	⊢ 0
12	9 10 11	cif	⊢ if ( 𝑥 ∈ 𝑎 , 1 , 0 )
13	6 4 12	cmpt	⊢ ( 𝑥 ∈ 𝑜 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) )
14	3 5 13	cmpt	⊢ ( 𝑎 ∈ 𝒫 𝑜 ↦ ( 𝑥 ∈ 𝑜 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) )
15	1 2 14	cmpt	⊢ ( 𝑜 ∈ V ↦ ( 𝑎 ∈ 𝒫 𝑜 ↦ ( 𝑥 ∈ 𝑜 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) )
16	0 15	wceq	⊢ 𝟭 = ( 𝑜 ∈ V ↦ ( 𝑎 ∈ 𝒫 𝑜 ↦ ( 𝑥 ∈ 𝑜 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) )