Description: Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en , which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | pw2f1o2.f | |- F = ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) |
|
| Assertion | pw2f1o2 | |- ( A e. V -> F : ( 2o ^m A ) -1-1-onto-> ~P A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pw2f1o2.f | |- F = ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) |
|
| 2 | 1 | pw2f1ocnv | |- ( A e. V -> ( F : ( 2o ^m A ) -1-1-onto-> ~P A /\ `' F = ( y e. ~P A |-> ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) ) ) |
| 3 | 2 | simpld | |- ( A e. V -> F : ( 2o ^m A ) -1-1-onto-> ~P A ) |