Definition df-image

Description: Define the image functor. This function takes a set A to a function x |-> ( A " x ) , providing that the latter exists. See imageval for the derivation. (Contributed by Scott Fenton, 27-Mar-2014)

	Ref	Expression
Assertion	df-image	⊢ Image 𝐴 = ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ ◡ 𝐴 ) ⊗ V ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	cimage	⊢ Image 𝐴
2		cvv	⊢ V
3	2 2	cxp	⊢ ( V × V )
4		cep	⊢ E
5	2 4	ctxp	⊢ ( V ⊗ E )
6	0	ccnv	⊢ ◡ 𝐴
7	4 6	ccom	⊢ ( E ∘ ◡ 𝐴 )
8	7 2	ctxp	⊢ ( ( E ∘ ◡ 𝐴 ) ⊗ V )
9	5 8	csymdif	⊢ ( ( V ⊗ E ) △ ( ( E ∘ ◡ 𝐴 ) ⊗ V ) )
10	9	crn	⊢ ran ( ( V ⊗ E ) △ ( ( E ∘ ◡ 𝐴 ) ⊗ V ) )
11	3 10	cdif	⊢ ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ ◡ 𝐴 ) ⊗ V ) ) )
12	1 11	wceq	⊢ Image 𝐴 = ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ ◡ 𝐴 ) ⊗ V ) ) )