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 31973

Description: Define the image function. See brimg 32044 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 31949	. 2 class Img
2		c2nd 7167	. . . . . 6 class 2^nd
3		c1st 7166	. . . . . 6 class 1^st
4	2, 3	ccom 5118	. . . . 5 class (2^nd ∘ 1^st )
5		cvv 3200	. . . . . . 7 class V
6	5, 5	cxp 5112	. . . . . 6 class (V × V)
7	3, 6	cres 5116	. . . . 5 class (1^st ↾ (V × V))
8	4, 7	cres 5116	. . . 4 class ((2^nd ∘ 1^st ) ↾ (1^st ↾ (V × V)))
9	8	cimage 31947	. . 3 class Image((2^nd ∘ 1^st ) ↾ (1^st ↾ (V × V)))
10		ccart 31948	. . 3 class Cart
11	9, 10	ccom 5118	. 2 class (Image((2^nd ∘ 1^st ) ↾ (1^st ↾ (V × V))) ∘ Cart)
12	1, 11	wceq 1483	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 32044

Copyright terms: Public domain