df-apply

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

		Ref	Expression
	Assertion	df-apply	$⊢ 𝖠𝗉𝗉𝗅𝗒 = (𝖡𝗂𝗀𝖼𝗎𝗉 \circ 𝖡𝗂𝗀𝖼𝗎𝗉) \circ (((V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))) \circ ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇)))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		capply	$class 𝖠𝗉𝗉𝗅𝗒$
1		cbigcup	$class 𝖡𝗂𝗀𝖼𝗎𝗉$
2	1 1	ccom	$class (𝖡𝗂𝗀𝖼𝗎𝗉 \circ 𝖡𝗂𝗀𝖼𝗎𝗉)$
3		cvv	$class V$
4	3 3	cxp	$class (V \times V)$
5		cep	$class E$
6	3 5	ctxp	$class (V \otimes E)$
7		csingles	$class 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌$
8	5 7	cres	$class ({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌})$
9	8 3	ctxp	$class (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V)$
10	6 9	csymdif	$class ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))$
11	10	crn	$class ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))$
12	4 11	cdif	$class ((V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V)))$
13		csingle	$class 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇$
14		cimg	$class 𝖨𝗆𝗀$
15	13 14	ccom	$class (𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀)$
16		cid	$class I$
17	16 13	cpprod	$class pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇)$
18	15 17	ccom	$class ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇))$
19	12 18	ccom	$class (((V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))) \circ ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇)))$
20	2 19	ccom	$class ((𝖡𝗂𝗀𝖼𝗎𝗉 \circ 𝖡𝗂𝗀𝖼𝗎𝗉) \circ (((V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))) \circ ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇))))$
21	0 20	wceq	$wff 𝖠𝗉𝗉𝗅𝗒 = (𝖡𝗂𝗀𝖼𝗎𝗉 \circ 𝖡𝗂𝗀𝖼𝗎𝗉) \circ (((V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))) \circ ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇)))$

Metamath Proof Explorer

Definition df-apply

Detailed syntax breakdown