Theorem 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	$$⊢\underset{\_}{Ⅎ}xA$$
	funimass4f.2	$$⊢\underset{\_}{Ⅎ}xB$$
	funimass4f.3	$$⊢\underset{\_}{Ⅎ}xF$$
Assertion	funimass4f	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to \left(F\left[A\right]\subseteq B\leftrightarrow \forall x\in AF\left(x\right)\in B\right)$$

Proof

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