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 35830

Description: Define the image function. See brimg 35901 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 35806	. 2 class Img
2		c2nd 8029	. . . . . 6 class 2^nd
3		c1st 8028	. . . . . 6 class 1^st
4	2, 3	ccom 5704	. . . . 5 class (2^nd ∘ 1^st )
5		cvv 3488	. . . . . . 7 class V
6	5, 5	cxp 5698	. . . . . 6 class (V × V)
7	3, 6	cres 5702	. . . . 5 class (1^st ↾ (V × V))
8	4, 7	cres 5702	. . . 4 class ((2^nd ∘ 1^st ) ↾ (1^st ↾ (V × V)))
9	8	cimage 35804	. . 3 class Image((2^nd ∘ 1^st ) ↾ (1^st ↾ (V × V)))
10		ccart 35805	. . 3 class Cart
11	9, 10	ccom 5704	. 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 35901

Copyright terms: Public domain