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$

Step	Hyp	Ref	Expression
1		difss	$⊢ (V \times V) ∖ ran ((V \otimes E) ∆ ((E \circ A^{-1}) \otimes V)) \subseteq V \times V$
2		df-rel	$⊢ Rel ((V \times V) ∖ ran ((V \otimes E) ∆ ((E \circ A^{-1}) \otimes V))) \leftrightarrow (V \times V) ∖ ran ((V \otimes E) ∆ ((E \circ A^{-1}) \otimes V)) \subseteq V \times V$
3	1 2	mpbir	$⊢ Rel ((V \times V) ∖ ran ((V \otimes E) ∆ ((E \circ A^{-1}) \otimes V)))$
4		df-image	$⊢ 𝖨𝗆𝖺𝗀𝖾 A = (V \times V) ∖ ran ((V \otimes E) ∆ ((E \circ A^{-1}) \otimes V))$
5	4	releqi	$⊢ Rel 𝖨𝗆𝖺𝗀𝖾 A \leftrightarrow Rel ((V \times V) ∖ ran ((V \otimes E) ∆ ((E \circ A^{-1}) \otimes V)))$
6	3 5	mpbir	$⊢ Rel 𝖨𝗆𝖺𝗀𝖾 A$
7		vex	$⊢ x \in V$
8		vex	$⊢ y \in V$
9	7 8	brimage	$⊢ x 𝖨𝗆𝖺𝗀𝖾 A y \leftrightarrow y = A [x]$
10		vex	$⊢ z \in V$
11	7 10	brimage	$⊢ x 𝖨𝗆𝖺𝗀𝖾 A z \leftrightarrow z = A [x]$
12		eqtr3	$⊢ (y = A [x] \land z = A [x]) \to y = z$
13	9 11 12	syl2anb	$⊢ (x 𝖨𝗆𝖺𝗀𝖾 A y \land x 𝖨𝗆𝖺𝗀𝖾 A z) \to y = z$
14	13	gen2	$⊢ \forall y \forall z ((x 𝖨𝗆𝖺𝗀𝖾 A y \land x 𝖨𝗆𝖺𝗀𝖾 A z) \to y = z)$
15	14	ax-gen	$⊢ \forall x \forall y \forall z ((x 𝖨𝗆𝖺𝗀𝖾 A y \land x 𝖨𝗆𝖺𝗀𝖾 A z) \to y = z)$
16		dffun2	$⊢ Fun 𝖨𝗆𝖺𝗀𝖾 A \leftrightarrow (Rel 𝖨𝗆𝖺𝗀𝖾 A \land \forall x \forall y \forall z ((x 𝖨𝗆𝖺𝗀𝖾 A y \land x 𝖨𝗆𝖺𝗀𝖾 A z) \to y = z))$
17	6 15 16	mpbir2an	$⊢ Fun 𝖨𝗆𝖺𝗀𝖾 A$

Metamath Proof Explorer