Definition df-img

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cimg	⊢ Img
1		c2nd	⊢ 2nd
2		c1st	⊢ 1st
3	1 2	ccom	⊢ ( 2nd ∘ 1st )
4		cvv	⊢ V
5	4 4	cxp	⊢ ( V × V )
6	2 5	cres	⊢ ( 1st ↾ ( V × V ) )
7	3 6	cres	⊢ ( ( 2nd ∘ 1st ) ↾ ( 1st ↾ ( V × V ) ) )
8	7	cimage	⊢ Image ( ( 2nd ∘ 1st ) ↾ ( 1st ↾ ( V × V ) ) )
9		ccart	⊢ Cart
10	8 9	ccom	⊢ ( Image ( ( 2nd ∘ 1st ) ↾ ( 1st ↾ ( V × V ) ) ) ∘ Cart )
11	0 10	wceq	⊢ Img = ( Image ( ( 2nd ∘ 1st ) ↾ ( 1st ↾ ( V × V ) ) ) ∘ Cart )