Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-apply Structured version   Visualization version   GIF version

Definition df-apply 35854
Description: Define the application function. See brapply 35919 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
StepHypRef Expression
1 capply 35826 . 2 class Apply
2 cbigcup 35815 . . . 4 class Bigcup
32, 2ccom 5692 . . 3 class ( Bigcup Bigcup )
4 cvv 3477 . . . . . 6 class V
54, 4cxp 5686 . . . . 5 class (V × V)
6 cep 5587 . . . . . . . 8 class E
74, 6ctxp 35811 . . . . . . 7 class (V ⊗ E )
8 csingles 35820 . . . . . . . . 9 class Singletons
96, 8cres 5690 . . . . . . . 8 class ( E ↾ Singletons )
109, 4ctxp 35811 . . . . . . 7 class (( E ↾ Singletons ) ⊗ V)
117, 10csymdif 4257 . . . . . 6 class ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))
1211crn 5689 . . . . 5 class ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))
135, 12cdif 3959 . . . 4 class ((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V)))
14 csingle 35819 . . . . . 6 class Singleton
15 cimg 35823 . . . . . 6 class Img
1614, 15ccom 5692 . . . . 5 class (Singleton ∘ Img)
17 cid 5581 . . . . . 6 class I
1817, 14cpprod 35812 . . . . 5 class pprod( I , Singleton)
1916, 18ccom 5692 . . . 4 class ((Singleton ∘ Img) ∘ pprod( I , Singleton))
2013, 19ccom 5692 . . 3 class (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton)))
213, 20ccom 5692 . 2 class (( Bigcup Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton))))
221, 21wceq 1536 1 wff Apply = (( Bigcup Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton))))
Colors of variables: wff setvar class
This definition is referenced by:  brapply  35919
  Copyright terms: Public domain W3C validator