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 33412
Description: Define the image function. See brimg 33483 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 33388 . 2 class Img
2 c2nd 7685 . . . . . 6 class 2nd
3 c1st 7684 . . . . . 6 class 1st
42, 3ccom 5547 . . . . 5 class (2nd ∘ 1st )
5 cvv 3480 . . . . . . 7 class V
65, 5cxp 5541 . . . . . 6 class (V × V)
73, 6cres 5545 . . . . 5 class (1st ↾ (V × V))
84, 7cres 5545 . . . 4 class ((2nd ∘ 1st ) ↾ (1st ↾ (V × V)))
98cimage 33386 . . 3 class Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V)))
10 ccart 33387 . . 3 class Cart
119, 10ccom 5547 . 2 class (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart)
121, 11wceq 1538 1 wff Img = (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart)
Colors of variables: wff setvar class
This definition is referenced by:  brimg  33483
  Copyright terms: Public domain W3C validator