This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) ) ) )