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 ( ( 2^nd ∘ 1^st ) ↾ ( 1^st ↾ ( V × V ) ) ) ∘ Cart )

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

Metamath Proof Explorer