Description: Define the image functor. This function takes a set A to a function x |-> ( A " x ) , providing that the latter exists. See imageval for the derivation. (Contributed by Scott Fenton, 27-Mar-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-image | |- Image A = ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. `' A ) (x) _V ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | |- A |
|
| 1 | 0 | cimage | |- Image A |
| 2 | cvv | |- _V |
|
| 3 | 2 2 | cxp | |- ( _V X. _V ) |
| 4 | cep | |- _E |
|
| 5 | 2 4 | ctxp | |- ( _V (x) _E ) |
| 6 | 0 | ccnv | |- `' A |
| 7 | 4 6 | ccom | |- ( _E o. `' A ) |
| 8 | 7 2 | ctxp | |- ( ( _E o. `' A ) (x) _V ) |
| 9 | 5 8 | csymdif | |- ( ( _V (x) _E ) /_\ ( ( _E o. `' A ) (x) _V ) ) |
| 10 | 9 | crn | |- ran ( ( _V (x) _E ) /_\ ( ( _E o. `' A ) (x) _V ) ) |
| 11 | 3 10 | cdif | |- ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. `' A ) (x) _V ) ) ) |
| 12 | 1 11 | wceq | |- Image A = ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. `' A ) (x) _V ) ) ) |