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 | |- _Ind = ( o e. _V |-> ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cind | |- _Ind |
|
| 1 | vo | |- o |
|
| 2 | cvv | |- _V |
|
| 3 | va | |- a |
|
| 4 | 1 | cv | |- o |
| 5 | 4 | cpw | |- ~P o |
| 6 | vx | |- x |
|
| 7 | 6 | cv | |- x |
| 8 | 3 | cv | |- a |
| 9 | 7 8 | wcel | |- x e. a |
| 10 | c1 | |- 1 |
|
| 11 | cc0 | |- 0 |
|
| 12 | 9 10 11 | cif | |- if ( x e. a , 1 , 0 ) |
| 13 | 6 4 12 | cmpt | |- ( x e. o |-> if ( x e. a , 1 , 0 ) ) |
| 14 | 3 5 13 | cmpt | |- ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) ) |
| 15 | 1 2 14 | cmpt | |- ( o e. _V |-> ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) ) ) |
| 16 | 0 15 | wceq | |- _Ind = ( o e. _V |-> ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) ) ) |