Definition df-apply 35510

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

Assertion

Ref	Expression
df-apply	⊢ Apply = (( Bigcup ∘ Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton))))

Detailed syntax breakdown of Definition df-apply

Step	Hyp	Ref	Expression
1		capply 35482	. 2 class Apply
2		cbigcup 35471	. . . 4 class Bigcup
3	2, 2	ccom 5686	. . 3 class ( Bigcup ∘ Bigcup )
4		cvv 3473	. . . . . 6 class V
5	4, 4	cxp 5680	. . . . 5 class (V × V)
6		cep 5585	. . . . . . . 8 class E
7	4, 6	ctxp 35467	. . . . . . 7 class (V ⊗ E )
8		csingles 35476	. . . . . . . . 9 class Singletons
9	6, 8	cres 5684	. . . . . . . 8 class ( E ↾ Singletons )
10	9, 4	ctxp 35467	. . . . . . 7 class (( E ↾ Singletons ) ⊗ V)
11	7, 10	csymdif 4244	. . . . . 6 class ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))
12	11	crn 5683	. . . . 5 class ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))
13	5, 12	cdif 3946	. . . 4 class ((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V)))
14		csingle 35475	. . . . . 6 class Singleton
15		cimg 35479	. . . . . 6 class Img
16	14, 15	ccom 5686	. . . . 5 class (Singleton ∘ Img)
17		cid 5579	. . . . . 6 class I
18	17, 14	cpprod 35468	. . . . 5 class pprod( I , Singleton)
19	16, 18	ccom 5686	. . . 4 class ((Singleton ∘ Img) ∘ pprod( I , Singleton))
20	13, 19	ccom 5686	. . 3 class (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton)))
21	3, 20	ccom 5686	. 2 class (( Bigcup ∘ Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton))))
22	1, 21	wceq 1533	1 wff Apply = (( Bigcup ∘ Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton))))

This definition is referenced by:  brapply  35575