Metamath Proof Explorer


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