Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Quantifier-free definitions
df-image
Metamath Proof Explorer
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 ) ) )