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 29401
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 29400 . 2 class 𝟭
2 vo . . 3 setvar 𝑜
3 cvv 3173 . . 3 class V
4 va . . . 4 setvar 𝑎
52cv 1474 . . . . 5 class 𝑜
65cpw 4108 . . . 4 class 𝒫 𝑜
7 vx . . . . 5 setvar 𝑥
87, 4wel 1978 . . . . . 6 wff 𝑥𝑎
9 c1 9816 . . . . . 6 class 1
10 cc0 9815 . . . . . 6 class 0
118, 9, 10cif 4036 . . . . 5 class if(𝑥𝑎, 1, 0)
127, 5, 11cmpt 4643 . . . 4 class (𝑥𝑜 ↦ if(𝑥𝑎, 1, 0))
134, 6, 12cmpt 4643 . . 3 class (𝑎 ∈ 𝒫 𝑜 ↦ (𝑥𝑜 ↦ if(𝑥𝑎, 1, 0)))
142, 3, 13cmpt 4643 . 2 class (𝑜 ∈ V ↦ (𝑎 ∈ 𝒫 𝑜 ↦ (𝑥𝑜 ↦ if(𝑥𝑎, 1, 0))))
151, 14wceq 1475 1 wff 𝟭 = (𝑜 ∈ V ↦ (𝑎 ∈ 𝒫 𝑜 ↦ (𝑥𝑜 ↦ if(𝑥𝑎, 1, 0))))
Colors of variables: wff setvar class
This definition is referenced by:  indv  29402
  Copyright terms: Public domain W3C validator