Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ind Structured version   Visualization version   GIF version

Definition df-ind 30047
 Description: Define the indicator function generator. (Contributed by Thierry Arnoux, 20-Jan-2017.)
Assertion
Ref Expression
df-ind 𝟭 = (𝑜 ∈ V ↦ (𝑎 ∈ 𝒫 𝑜 ↦ (𝑥𝑜 ↦ if(𝑥𝑎, 1, 0))))
Distinct variable group:   𝑜,𝑎,𝑥

Detailed syntax breakdown of Definition df-ind
StepHypRef Expression
1 cind 30046 . 2 class 𝟭
2 vo . . 3 setvar 𝑜
3 cvv 3195 . . 3 class V
4 va . . . 4 setvar 𝑎
52cv 1480 . . . . 5 class 𝑜
65cpw 4149 . . . 4 class 𝒫 𝑜
7 vx . . . . 5 setvar 𝑥
87, 4wel 1989 . . . . . 6 wff 𝑥𝑎
9 c1 9922 . . . . . 6 class 1
10 cc0 9921 . . . . . 6 class 0
118, 9, 10cif 4077 . . . . 5 class if(𝑥𝑎, 1, 0)
127, 5, 11cmpt 4720 . . . 4 class (𝑥𝑜 ↦ if(𝑥𝑎, 1, 0))
134, 6, 12cmpt 4720 . . 3 class (𝑎 ∈ 𝒫 𝑜 ↦ (𝑥𝑜 ↦ if(𝑥𝑎, 1, 0)))
142, 3, 13cmpt 4720 . 2 class (𝑜 ∈ V ↦ (𝑎 ∈ 𝒫 𝑜 ↦ (𝑥𝑜 ↦ if(𝑥𝑎, 1, 0))))
151, 14wceq 1481 1 wff 𝟭 = (𝑜 ∈ V ↦ (𝑎 ∈ 𝒫 𝑜 ↦ (𝑥𝑜 ↦ if(𝑥𝑎, 1, 0))))
 Colors of variables: wff setvar class This definition is referenced by:  indv  30048
 Copyright terms: Public domain W3C validator