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 ⊢ 𝖨𝗆𝖺𝗀𝖾 A = V × V ∖ ran ⁡ V ⊗ E ∆ E ∘ A -1 ⊗ V

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 0 cimage class 𝖨𝗆𝖺𝗀𝖾 A
2 cvv class V
3 2 2 cxp class V × V
4 cep class E
5 2 4 ctxp class V ⊗ E
6 0 ccnv class A -1
7 4 6 ccom class E ∘ A -1
8 7 2 ctxp class E ∘ A -1 ⊗ V
9 5 8 csymdif class V ⊗ E ∆ E ∘ A -1 ⊗ V
10 9 crn class ran ⁡ V ⊗ E ∆ E ∘ A -1 ⊗ V
11 3 10 cdif class V × V ∖ ran ⁡ V ⊗ E ∆ E ∘ A -1 ⊗ V
12 1 11 wceq wff 𝖨𝗆𝖺𝗀𝖾 A = V × V ∖ ran ⁡ V ⊗ E ∆ E ∘ A -1 ⊗ V