Metamath Proof Explorer


Theorem funimage

Description: Image A is a function. (Contributed by Scott Fenton, 27-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion funimage Fun 𝖨𝗆𝖺𝗀𝖾 A

Proof

Step Hyp Ref Expression
1 difss V × V ran V E E A -1 V V × V
2 df-rel Rel V × V ran V E E A -1 V V × V ran V E E A -1 V V × V
3 1 2 mpbir Rel V × V ran V E E A -1 V
4 df-image 𝖨𝗆𝖺𝗀𝖾 A = V × V ran V E E A -1 V
5 4 releqi Rel 𝖨𝗆𝖺𝗀𝖾 A Rel V × V ran V E E A -1 V
6 3 5 mpbir Rel 𝖨𝗆𝖺𝗀𝖾 A
7 vex x V
8 vex y V
9 7 8 brimage x 𝖨𝗆𝖺𝗀𝖾 A y y = A x
10 vex z V
11 7 10 brimage x 𝖨𝗆𝖺𝗀𝖾 A z z = A x
12 eqtr3 y = A x z = A x y = z
13 9 11 12 syl2anb x 𝖨𝗆𝖺𝗀𝖾 A y x 𝖨𝗆𝖺𝗀𝖾 A z y = z
14 13 gen2 y z x 𝖨𝗆𝖺𝗀𝖾 A y x 𝖨𝗆𝖺𝗀𝖾 A z y = z
15 14 ax-gen x y z x 𝖨𝗆𝖺𝗀𝖾 A y x 𝖨𝗆𝖺𝗀𝖾 A z y = z
16 dffun2 Fun 𝖨𝗆𝖺𝗀𝖾 A Rel 𝖨𝗆𝖺𝗀𝖾 A x y z x 𝖨𝗆𝖺𝗀𝖾 A y x 𝖨𝗆𝖺𝗀𝖾 A z y = z
17 6 15 16 mpbir2an Fun 𝖨𝗆𝖺𝗀𝖾 A