Users' Mathboxes 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 29203
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 29202 . 2 class 𝟭
2 vo . . 3 setvar 𝑜
3 cvv 3168 . . 3 class V
4 va . . . 4 setvar 𝑎
52cv 1473 . . . . 5 class 𝑜
65cpw 4103 . . . 4 class 𝒫 𝑜
7 vx . . . . 5 setvar 𝑥
87, 4wel 1976 . . . . . 6 wff 𝑥𝑎
9 c1 9789 . . . . . 6 class 1
10 cc0 9788 . . . . . 6 class 0
118, 9, 10cif 4031 . . . . 5 class if(𝑥𝑎, 1, 0)
127, 5, 11cmpt 4633 . . . 4 class (𝑥𝑜 ↦ if(𝑥𝑎, 1, 0))
134, 6, 12cmpt 4633 . . 3 class (𝑎 ∈ 𝒫 𝑜 ↦ (𝑥𝑜 ↦ if(𝑥𝑎, 1, 0)))
142, 3, 13cmpt 4633 . 2 class (𝑜 ∈ V ↦ (𝑎 ∈ 𝒫 𝑜 ↦ (𝑥𝑜 ↦ if(𝑥𝑎, 1, 0))))
151, 14wceq 1474 1 wff 𝟭 = (𝑜 ∈ V ↦ (𝑎 ∈ 𝒫 𝑜 ↦ (𝑥𝑜 ↦ if(𝑥𝑎, 1, 0))))
Colors of variables: wff setvar class
This definition is referenced by:  indv  29204
  Copyright terms: Public domain W3C validator