funimass4f

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017)

	Ref	Expression
Hypotheses	funimass4f.1	$⊢ \underline{Ⅎ} x A$
	funimass4f.2	$⊢ \underline{Ⅎ} x B$
	funimass4f.3	$⊢ \underline{Ⅎ} x F$
Assertion	funimass4f	$⊢ (Fun F \land A \subseteq dom F) \to (F [A] \subseteq B \leftrightarrow \forall x \in A F (x) \in B)$

Step	Hyp	Ref	Expression
1		funimass4f.1	$⊢ \underline{Ⅎ} x A$
2		funimass4f.2	$⊢ \underline{Ⅎ} x B$
3		funimass4f.3	$⊢ \underline{Ⅎ} x F$
4	3	nffun	$⊢ Ⅎ x Fun F$
5	3	nfdm	$⊢ \underline{Ⅎ} x dom F$
6	1 5	nfss	$⊢ Ⅎ x A \subseteq dom F$
7	4 6	nfan	$⊢ Ⅎ x (Fun F \land A \subseteq dom F)$
8	3 1	nfima	$⊢ \underline{Ⅎ} x F [A]$
9	8 2	nfss	$⊢ Ⅎ x F [A] \subseteq B$
10	7 9	nfan	$⊢ Ⅎ x ((Fun F \land A \subseteq dom F) \land F [A] \subseteq B)$
11		funfvima2	$⊢ (Fun F \land A \subseteq dom F) \to (x \in A \to F (x) \in F [A])$
12		ssel	$⊢ F [A] \subseteq B \to (F (x) \in F [A] \to F (x) \in B)$
13	11 12	sylan9	$⊢ ((Fun F \land A \subseteq dom F) \land F [A] \subseteq B) \to (x \in A \to F (x) \in B)$
14	10 13	ralrimi	$⊢ ((Fun F \land A \subseteq dom F) \land F [A] \subseteq B) \to \forall x \in A F (x) \in B$
15	1 3	dfimafnf	$⊢ (Fun F \land A \subseteq dom F) \to F [A] = \{y \| \exists x \in A y = F (x)\}$
16	15	adantr	$⊢ ((Fun F \land A \subseteq dom F) \land \forall x \in A F (x) \in B) \to F [A] = \{y \| \exists x \in A y = F (x)\}$
17	2	abrexss	$⊢ \forall x \in A F (x) \in B \to \{y \| \exists x \in A y = F (x)\} \subseteq B$
18	17	adantl	$⊢ ((Fun F \land A \subseteq dom F) \land \forall x \in A F (x) \in B) \to \{y \| \exists x \in A y = F (x)\} \subseteq B$
19	16 18	eqsstrd	$⊢ ((Fun F \land A \subseteq dom F) \land \forall x \in A F (x) \in B) \to F [A] \subseteq B$
20	14 19	impbida	$⊢ (Fun F \land A \subseteq dom F) \to (F [A] \subseteq B \leftrightarrow \forall x \in A F (x) \in B)$

Metamath Proof Explorer