dfimafnf

Description: Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006) (Revised by Thierry Arnoux, 24-Apr-2017)

	Ref	Expression
Hypotheses	dfimafnf.1	$⊢ \underline{Ⅎ} x A$
	dfimafnf.2	$⊢ \underline{Ⅎ} x F$
Assertion	dfimafnf	$⊢ (Fun F \land A \subseteq dom F) \to F [A] = \{y \| \exists x \in A y = F (x)\}$

Proof

Step	Hyp	Ref	Expression
1		dfimafnf.1	$⊢ \underline{Ⅎ} x A$
2		dfimafnf.2	$⊢ \underline{Ⅎ} x F$
3		dfima2	$⊢ F [A] = \{y \| \exists z \in A z F y\}$
4		ssel	$⊢ A \subseteq dom F \to (z \in A \to z \in dom F)$
5		eqcom	$⊢ F (z) = y \leftrightarrow y = F (z)$
6		funbrfvb	$⊢ (Fun F \land z \in dom F) \to (F (z) = y \leftrightarrow z F y)$
7	5 6	bitr3id	$⊢ (Fun F \land z \in dom F) \to (y = F (z) \leftrightarrow z F y)$
8	7	ex	$⊢ Fun F \to (z \in dom F \to (y = F (z) \leftrightarrow z F y))$
9	4 8	syl9r	$⊢ Fun F \to (A \subseteq dom F \to (z \in A \to (y = F (z) \leftrightarrow z F y)))$
10	9	imp31	$⊢ ((Fun F \land A \subseteq dom F) \land z \in A) \to (y = F (z) \leftrightarrow z F y)$
11	10	rexbidva	$⊢ (Fun F \land A \subseteq dom F) \to (\exists z \in A y = F (z) \leftrightarrow \exists z \in A z F y)$
12	11	abbidv	$⊢ (Fun F \land A \subseteq dom F) \to \{y \| \exists z \in A y = F (z)\} = \{y \| \exists z \in A z F y\}$
13	3 12	eqtr4id	$⊢ (Fun F \land A \subseteq dom F) \to F [A] = \{y \| \exists z \in A y = F (z)\}$
14		nfcv	$⊢ \underline{Ⅎ} z A$
15		nfcv	$⊢ \underline{Ⅎ} x z$
16	2 15	nffv	$⊢ \underline{Ⅎ} x F (z)$
17	16	nfeq2	$⊢ Ⅎ x y = F (z)$
18		nfv	$⊢ Ⅎ z y = F (x)$
19		fveq2	$⊢ z = x \to F (z) = F (x)$
20	19	eqeq2d	$⊢ z = x \to (y = F (z) \leftrightarrow y = F (x))$
21	14 1 17 18 20	cbvrexfw	$⊢ \exists z \in A y = F (z) \leftrightarrow \exists x \in A y = F (x)$
22	21	abbii	$⊢ \{y \| \exists z \in A y = F (z)\} = \{y \| \exists x \in A y = F (x)\}$
23	13 22	eqtrdi	$⊢ (Fun F \land A \subseteq dom F) \to F [A] = \{y \| \exists x \in A y = F (x)\}$

Metamath Proof Explorer

Theorem dfimafnf

Proof