Definition df-apply 35378

Description: Define the application function. See brapply 35443 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 35350	. 2 class Apply
2		cbigcup 35339	. . . 4 class Bigcup
3	2, 2	ccom 5673	. . 3 class ( Bigcup ∘ Bigcup )
4		cvv 3468	. . . . . 6 class V
5	4, 4	cxp 5667	. . . . 5 class (V × V)
6		cep 5572	. . . . . . . 8 class E
7	4, 6	ctxp 35335	. . . . . . 7 class (V ⊗ E )
8		csingles 35344	. . . . . . . . 9 class Singletons
9	6, 8	cres 5671	. . . . . . . 8 class ( E ↾ Singletons )
10	9, 4	ctxp 35335	. . . . . . 7 class (( E ↾ Singletons ) ⊗ V)
11	7, 10	csymdif 4236	. . . . . 6 class ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))
12	11	crn 5670	. . . . 5 class ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))
13	5, 12	cdif 3940	. . . 4 class ((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V)))
14		csingle 35343	. . . . . 6 class Singleton
15		cimg 35347	. . . . . 6 class Img
16	14, 15	ccom 5673	. . . . 5 class (Singleton ∘ Img)
17		cid 5566	. . . . . 6 class I
18	17, 14	cpprod 35336	. . . . 5 class pprod( I , Singleton)
19	16, 18	ccom 5673	. . . 4 class ((Singleton ∘ Img) ∘ pprod( I , Singleton))
20	13, 19	ccom 5673	. . 3 class (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton)))
21	3, 20	ccom 5673	. 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  35443