df-img

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

		Ref	Expression
	Assertion	df-img	$⊢ 𝖨𝗆𝗀 = 𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) \circ 𝖢𝖺𝗋𝗍$

Step	Hyp	Ref	Expression
0		cimg	$class 𝖨𝗆𝗀$
1		c2nd	$class 2^{nd}$
2		c1st	$class 1^{st}$
3	1 2	ccom	$class (2^{nd} \circ 1^{st})$
4		cvv	$class V$
5	4 4	cxp	$class (V \times V)$
6	2 5	cres	$class ({1^{st} ↾}_{(V \times V)})$
7	3 6	cres	$class ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})})$
8	7	cimage	$class 𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})})$
9		ccart	$class 𝖢𝖺𝗋𝗍$
10	8 9	ccom	$class (𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) \circ 𝖢𝖺𝗋𝗍)$
11	0 10	wceq	$wff 𝖨𝗆𝗀 = 𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) \circ 𝖢𝖺𝗋𝗍$

Metamath Proof Explorer