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 33327

Description: Define the image function. See brimg 33398 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 33303	. 2 class Img
2		c2nd 7688	. . . . . 6 class 2^nd
3		c1st 7687	. . . . . 6 class 1^st
4	2, 3	ccom 5559	. . . . 5 class (2^nd ∘ 1^st )
5		cvv 3494	. . . . . . 7 class V
6	5, 5	cxp 5553	. . . . . 6 class (V × V)
7	3, 6	cres 5557	. . . . 5 class (1^st ↾ (V × V))
8	4, 7	cres 5557	. . . 4 class ((2^nd ∘ 1^st ) ↾ (1^st ↾ (V × V)))
9	8	cimage 33301	. . 3 class Image((2^nd ∘ 1^st ) ↾ (1^st ↾ (V × V)))
10		ccart 33302	. . 3 class Cart
11	9, 10	ccom 5559	. 2 class (Image((2^nd ∘ 1^st ) ↾ (1^st ↾ (V × V))) ∘ Cart)
12	1, 11	wceq 1537	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 33398

Copyright terms: Public domain