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