Users' Mathboxes 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 33224
Description: Define the image function. See brimg 33295 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 33200 . 2 class Img
2 c2nd 7677 . . . . . 6 class 2nd
3 c1st 7676 . . . . . 6 class 1st
42, 3ccom 5552 . . . . 5 class (2nd ∘ 1st )
5 cvv 3492 . . . . . . 7 class V
65, 5cxp 5546 . . . . . 6 class (V × V)
73, 6cres 5550 . . . . 5 class (1st ↾ (V × V))
84, 7cres 5550 . . . 4 class ((2nd ∘ 1st ) ↾ (1st ↾ (V × V)))
98cimage 33198 . . 3 class Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V)))
10 ccart 33199 . . 3 class Cart
119, 10ccom 5552 . 2 class (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart)
121, 11wceq 1528 1 wff Img = (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart)
Colors of variables: wff setvar class
This definition is referenced by:  brimg  33295
  Copyright terms: Public domain W3C validator