df-img - Mathbox for Scott Fenton

	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 35867

Description: Define the image function. See brimg 35938 for its value. (Contributed by Scott Fenton, 12-Apr-2014.)

**Assertion**
Ref	Expression
df-img	⊢ Img = (Image((2^nd ∘ 1^st ) ↾ (1^st ↾ (V × V))) ∘ Cart)

**Detailed syntax breakdown of Definition df-img**
Step	Hyp	Ref	Expression
1		cimg 35843	. 2 class Img
2		c2nd 8013	. . . . . 6 class 2^nd
3		c1st 8012	. . . . . 6 class 1^st
4	2, 3	ccom 5689	. . . . 5 class (2^nd ∘ 1^st )
5		cvv 3480	. . . . . . 7 class V
6	5, 5	cxp 5683	. . . . . 6 class (V × V)
7	3, 6	cres 5687	. . . . 5 class (1^st ↾ (V × V))
8	4, 7	cres 5687	. . . 4 class ((2^nd ∘ 1^st ) ↾ (1^st ↾ (V × V)))
9	8	cimage 35841	. . 3 class Image((2^nd ∘ 1^st ) ↾ (1^st ↾ (V × V)))
10		ccart 35842	. . 3 class Cart
11	9, 10	ccom 5689	. 2 class (Image((2^nd ∘ 1^st ) ↾ (1^st ↾ (V × V))) ∘ Cart)
12	1, 11	wceq 1540	1 wff Img = (Image((2^nd ∘ 1^st ) ↾ (1^st ↾ (V × V))) ∘ Cart)

Colors of variables: wff setvar class

This definition is referenced by: brimg 35938

Copyright terms: Public domain