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 | ⊢ 𝟭 = ( 𝑜 ∈ V ↦ ( 𝑎 ∈ 𝒫 𝑜 ↦ ( 𝑥 ∈ 𝑜 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) ) |
| 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 ) ) ) ) |