fimarab

Description: Expressing the image of a set as a restricted abstract builder. (Contributed by Thierry Arnoux, 27-Jan-2020)

		Ref	Expression
	Assertion	fimarab	$⊢ (F : A ⟶ B \land X \subseteq A) \to F [X] = \{y \in B \| \exists x \in X F (x) = y\}$

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ y (F : A ⟶ B \land X \subseteq A)$
2		nfcv	$⊢ \underline{Ⅎ} y F [X]$
3		nfrab1	$⊢ \underline{Ⅎ} y \{y \in B \| \exists x \in X F (x) = y\}$
4		ffn	$⊢ F : A ⟶ B \to F Fn A$
5		fvelimab	$⊢ (F Fn A \land X \subseteq A) \to (y \in F [X] \leftrightarrow \exists x \in X F (x) = y)$
6	5	anbi2d	$⊢ (F Fn A \land X \subseteq A) \to ((y \in B \land y \in F [X]) \leftrightarrow (y \in B \land \exists x \in X F (x) = y))$
7	4 6	sylan	$⊢ (F : A ⟶ B \land X \subseteq A) \to ((y \in B \land y \in F [X]) \leftrightarrow (y \in B \land \exists x \in X F (x) = y))$
8		fimass	$⊢ F : A ⟶ B \to F [X] \subseteq B$
9	8	adantr	$⊢ (F : A ⟶ B \land X \subseteq A) \to F [X] \subseteq B$
10	9	sseld	$⊢ (F : A ⟶ B \land X \subseteq A) \to (y \in F [X] \to y \in B)$
11	10	pm4.71rd	$⊢ (F : A ⟶ B \land X \subseteq A) \to (y \in F [X] \leftrightarrow (y \in B \land y \in F [X]))$
12		rabid	$⊢ y \in \{y \in B \| \exists x \in X F (x) = y\} \leftrightarrow (y \in B \land \exists x \in X F (x) = y)$
13	12	a1i	$⊢ (F : A ⟶ B \land X \subseteq A) \to (y \in \{y \in B \| \exists x \in X F (x) = y\} \leftrightarrow (y \in B \land \exists x \in X F (x) = y))$
14	7 11 13	3bitr4d	$⊢ (F : A ⟶ B \land X \subseteq A) \to (y \in F [X] \leftrightarrow y \in \{y \in B \| \exists x \in X F (x) = y\})$
15	1 2 3 14	eqrd	$⊢ (F : A ⟶ B \land X \subseteq A) \to F [X] = \{y \in B \| \exists x \in X F (x) = y\}$

Metamath Proof Explorer