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

Definition df-img 31142
 Description: Define the image function. See brimg 31214 for its value. (Contributed by Scott Fenton, 12-Apr-2014.)
Assertion
Ref Expression
df-img Img = (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart)

Detailed syntax breakdown of Definition df-img
StepHypRef Expression
1 cimg 31118 . 2 class Img
2 c2nd 7058 . . . . . 6 class 2nd
3 c1st 7057 . . . . . 6 class 1st
42, 3ccom 5042 . . . . 5 class (2nd ∘ 1st )
5 cvv 3173 . . . . . . 7 class V
65, 5cxp 5036 . . . . . 6 class (V × V)
73, 6cres 5040 . . . . 5 class (1st ↾ (V × V))
84, 7cres 5040 . . . 4 class ((2nd ∘ 1st ) ↾ (1st ↾ (V × V)))
98cimage 31116 . . 3 class Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V)))
10 ccart 31117 . . 3 class Cart
119, 10ccom 5042 . 2 class (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart)
121, 11wceq 1475 1 wff Img = (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart)
 Colors of variables: wff setvar class This definition is referenced by:  brimg  31214
 Copyright terms: Public domain W3C validator