![]() |
Mathbox for Scott Fenton |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-image | Structured version Visualization version GIF version |
Description: Define the image functor. This function takes a set 𝐴 to a function 𝑥 ↦ (𝐴 “ 𝑥), providing that the latter exists. See imageval 34902 for the derivation. (Contributed by Scott Fenton, 27-Mar-2014.) |
Ref | Expression |
---|---|
df-image | ⊢ Image𝐴 = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | cimage 34812 | . 2 class Image𝐴 |
3 | cvv 3475 | . . . 4 class V | |
4 | 3, 3 | cxp 5675 | . . 3 class (V × V) |
5 | cep 5580 | . . . . . 6 class E | |
6 | 3, 5 | ctxp 34802 | . . . . 5 class (V ⊗ E ) |
7 | 1 | ccnv 5676 | . . . . . . 7 class ◡𝐴 |
8 | 5, 7 | ccom 5681 | . . . . . 6 class ( E ∘ ◡𝐴) |
9 | 8, 3 | ctxp 34802 | . . . . 5 class (( E ∘ ◡𝐴) ⊗ V) |
10 | 6, 9 | csymdif 4242 | . . . 4 class ((V ⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V)) |
11 | 10 | crn 5678 | . . 3 class ran ((V ⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V)) |
12 | 4, 11 | cdif 3946 | . 2 class ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V))) |
13 | 2, 12 | wceq 1542 | 1 wff Image𝐴 = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V))) |
Colors of variables: wff setvar class |
This definition is referenced by: brimage 34898 funimage 34900 |
Copyright terms: Public domain | W3C validator |