Definition df-img 34196

Description: Define the image function. See brimg 34267 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

Step	Hyp	Ref	Expression
1		cimg 34172	. 2 class Img
2		c2nd 7850	. . . . . 6 class 2nd
3		c1st 7849	. . . . . 6 class 1st
4	2, 3	ccom 5595	. . . . 5 class (2nd ∘ 1st )
5		cvv 3434	. . . . . . 7 class V
6	5, 5	cxp 5589	. . . . . 6 class (V × V)
7	3, 6	cres 5593	. . . . 5 class (1st ↾ (V × V))
8	4, 7	cres 5593	. . . 4 class ((2nd ∘ 1st ) ↾ (1st ↾ (V × V)))
9	8	cimage 34170	. . 3 class Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V)))
10		ccart 34171	. . 3 class Cart
11	9, 10	ccom 5595	. 2 class (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart)
12	1, 11	wceq 1537	1 wff Img = (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart)

This definition is referenced by:  brimg  34267