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	⊢ Apply = ( ( Bigcup ∘ Bigcup ) ∘ ( ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) ) ∘ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		capply	⊢ Apply
1		cbigcup	⊢ Bigcup
2	1 1	ccom	⊢ ( Bigcup ∘ Bigcup )
3		cvv	⊢ V
4	3 3	cxp	⊢ ( V × V )
5		cep	⊢ E
6	3 5	ctxp	⊢ ( V ⊗ E )
7		csingles	⊢ Singletons
8	5 7	cres	⊢ ( E ↾ Singletons )
9	8 3	ctxp	⊢ ( ( E ↾ Singletons ) ⊗ V )
10	6 9	csymdif	⊢ ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) )
11	10	crn	⊢ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) )
12	4 11	cdif	⊢ ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) )
13		csingle	⊢ Singleton
14		cimg	⊢ Img
15	13 14	ccom	⊢ ( Singleton ∘ Img )
16		cid	⊢ I
17	16 13	cpprod	⊢ pprod ( I , Singleton )
18	15 17	ccom	⊢ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) )
19	12 18	ccom	⊢ ( ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) ) ∘ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) ) )
20	2 19	ccom	⊢ ( ( Bigcup ∘ Bigcup ) ∘ ( ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) ) ∘ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) ) ) )
21	0 20	wceq	⊢ Apply = ( ( Bigcup ∘ Bigcup ) ∘ ( ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) ) ∘ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) ) ) )