Metamath Proof Explorer


Definition df-apply

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

Ref Expression
Assertion df-apply 𝖠𝗉𝗉𝗅𝗒 = 𝖡𝗂𝗀𝖼𝗎𝗉 𝖡𝗂𝗀𝖼𝗎𝗉 V × V ran V E E 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 V 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 𝖨𝗆𝗀 pprod I 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇

Detailed syntax breakdown

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