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

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 Image 𝐴

Proof

Step Hyp Ref Expression
1 difss ⊢ ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ ◡ 𝐴 ) ⊗ V ) ) ) ⊆ ( V × V )
2 df-rel ⊢ ( Rel ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ ◡ 𝐴 ) ⊗ V ) ) ) ↔ ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ ◡ 𝐴 ) ⊗ V ) ) ) ⊆ ( V × V ) )
3 1 2 mpbir ⊢ Rel ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ ◡ 𝐴 ) ⊗ V ) ) )
4 df-image ⊢ Image 𝐴 = ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ ◡ 𝐴 ) ⊗ V ) ) )
5 4 releqi ⊢ ( Rel Image 𝐴 ↔ Rel ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ ◡ 𝐴 ) ⊗ V ) ) ) )
6 3 5 mpbir ⊢ Rel Image 𝐴
7 vex ⊢ 𝑥 ∈ V
8 vex ⊢ 𝑦 ∈ V
9 7 8 brimage ⊢ ( 𝑥 Image 𝐴 𝑦 ↔ 𝑦 = ( 𝐴 “ 𝑥 ) )
10 vex ⊢ 𝑧 ∈ V
11 7 10 brimage ⊢ ( 𝑥 Image 𝐴 𝑧 ↔ 𝑧 = ( 𝐴 “ 𝑥 ) )
12 eqtr3 ⊢ ( ( 𝑦 = ( 𝐴 “ 𝑥 ) ∧ 𝑧 = ( 𝐴 “ 𝑥 ) ) → 𝑦 = 𝑧 )
13 9 11 12 syl2anb ⊢ ( ( 𝑥 Image 𝐴 𝑦 ∧ 𝑥 Image 𝐴 𝑧 ) → 𝑦 = 𝑧 )
14 13 gen2 ⊢ ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 Image 𝐴 𝑦 ∧ 𝑥 Image 𝐴 𝑧 ) → 𝑦 = 𝑧 )
15 14 ax-gen ⊢ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 Image 𝐴 𝑦 ∧ 𝑥 Image 𝐴 𝑧 ) → 𝑦 = 𝑧 )
16 dffun2 ⊢ ( Fun Image 𝐴 ↔ ( Rel Image 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 Image 𝐴 𝑦 ∧ 𝑥 Image 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ) )
17 6 15 16 mpbir2an ⊢ Fun Image 𝐴