Definition df-img 34095

Description: Define the image function. See brimg 34166 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 34071	. 2 class Img
2		c2nd 7803	. . . . . 6 class 2nd
3		c1st 7802	. . . . . 6 class 1st
4	2, 3	ccom 5584	. . . . 5 class (2nd ∘ 1st )
5		cvv 3422	. . . . . . 7 class V
6	5, 5	cxp 5578	. . . . . 6 class (V × V)
7	3, 6	cres 5582	. . . . 5 class (1st ↾ (V × V))
8	4, 7	cres 5582	. . . 4 class ((2nd ∘ 1st ) ↾ (1st ↾ (V × V)))
9	8	cimage 34069	. . 3 class Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V)))
10		ccart 34070	. . 3 class Cart
11	9, 10	ccom 5584	. 2 class (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart)
12	1, 11	wceq 1539	1 wff Img = (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart)

This definition is referenced by:  brimg  34166