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 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇