Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-image Structured version   Visualization version   GIF version

Definition df-image 33222
Description: Define the image functor. This function takes a set 𝐴 to a function 𝑥 ↦ (𝐴𝑥), providing that the latter exists. See imageval 33288 for the derivation. (Contributed by Scott Fenton, 27-Mar-2014.)
Assertion
Ref Expression
df-image Image𝐴 = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ 𝐴) ⊗ V)))

Detailed syntax breakdown of Definition df-image
StepHypRef Expression
1 cA . . 3 class 𝐴
21cimage 33198 . 2 class Image𝐴
3 cvv 3492 . . . 4 class V
43, 3cxp 5546 . . 3 class (V × V)
5 cep 5457 . . . . . 6 class E
63, 5ctxp 33188 . . . . 5 class (V ⊗ E )
71ccnv 5547 . . . . . . 7 class 𝐴
85, 7ccom 5552 . . . . . 6 class ( E ∘ 𝐴)
98, 3ctxp 33188 . . . . 5 class (( E ∘ 𝐴) ⊗ V)
106, 9csymdif 4215 . . . 4 class ((V ⊗ E ) △ (( E ∘ 𝐴) ⊗ V))
1110crn 5549 . . 3 class ran ((V ⊗ E ) △ (( E ∘ 𝐴) ⊗ V))
124, 11cdif 3930 . 2 class ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ 𝐴) ⊗ V)))
132, 12wceq 1528 1 wff Image𝐴 = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ 𝐴) ⊗ V)))
Colors of variables: wff setvar class
This definition is referenced by:  brimage  33284  funimage  33286
  Copyright terms: Public domain W3C validator