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 𝐴