Metamath Proof Explorer

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 o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) o. Cart )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cimg 
 |-  Img
1 c2nd 
 |-  2nd
2 c1st 
 |-  1st
3 1 2 ccom 
 |-  ( 2nd o. 1st )
4 cvv 
 |-  _V
5 4 4 cxp 
 |-  ( _V X. _V )
6 2 5 cres 
 |-  ( 1st |` ( _V X. _V ) )
7 3 6 cres 
 |-  ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) )
8 7 cimage 
 |-  Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) )
9 ccart 
 |-  Cart
10 8 9 ccom 
 |-  ( Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) o. Cart )
11 0 10 wceq 
 |-  Img = ( Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) o. Cart )