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

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