Theorem fvmptss

Description: If all the values of the mapping are subsets of a class C , then so is any evaluation of the mapping, even if D is not in the base set A . (Contributed by Mario Carneiro, 13-Feb-2015)

	Ref	Expression
Hypothesis	mptrcl.1	$$⊢F=\left(x\in A⟼B\right)$$
Assertion	fvmptss	$$⊢\forall x\in AB\subseteq C\to F\left(D\right)\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		mptrcl.1	$$⊢F=\left(x\in A⟼B\right)$$
2	1	dmmptss	$$⊢\mathrm{dom}F\subseteq A$$
3	2	sseli	$$⊢D\in \mathrm{dom}F\to D\in A$$
4		fveq2	$$⊢y=D\to F\left(y\right)=F\left(D\right)$$
5	4	sseq1d	$$⊢y=D\to \left(F\left(y\right)\subseteq C\leftrightarrow F\left(D\right)\subseteq C\right)$$
6	5	imbi2d	$$⊢y=D\to \left(\left(\forall x\in AB\subseteq C\to F\left(y\right)\subseteq C\right)\leftrightarrow \left(\forall x\in AB\subseteq C\to F\left(D\right)\subseteq C\right)\right)$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
8		nfra1	$$⊢Ⅎx\forall x\in AB\subseteq C$$
9		nfmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in A⟼B\right)$$
10	1 9	nfcxfr	$$⊢\underset{\_}{Ⅎ}xF$$
11	10 7	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(y\right)$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}xC$$
13	11 12	nfss	$$⊢ℲxF\left(y\right)\subseteq C$$
14	8 13	nfim	$$⊢Ⅎx\left(\forall x\in AB\subseteq C\to F\left(y\right)\subseteq C\right)$$
15		fveq2	$$⊢x=y\to F\left(x\right)=F\left(y\right)$$
16	15	sseq1d	$$⊢x=y\to \left(F\left(x\right)\subseteq C\leftrightarrow F\left(y\right)\subseteq C\right)$$
17	16	imbi2d	$$⊢x=y\to \left(\left(\forall x\in AB\subseteq C\to F\left(x\right)\subseteq C\right)\leftrightarrow \left(\forall x\in AB\subseteq C\to F\left(y\right)\subseteq C\right)\right)$$
18	1	dmmpt	$$⊢\mathrm{dom}F=\left\{x\in A|B\in \mathrm{V}\right\}$$
19	18	reqabi	$$⊢x\in \mathrm{dom}F\leftrightarrow \left(x\in A\wedge B\in \mathrm{V}\right)$$
20	1	fvmpt2	$$⊢\left(x\in A\wedge B\in \mathrm{V}\right)\to F\left(x\right)=B$$
21		eqimss	$$⊢F\left(x\right)=B\to F\left(x\right)\subseteq B$$
22	20 21	syl	$$⊢\left(x\in A\wedge B\in \mathrm{V}\right)\to F\left(x\right)\subseteq B$$
23	19 22	sylbi	$$⊢x\in \mathrm{dom}F\to F\left(x\right)\subseteq B$$
24		ndmfv	$$⊢\neg x\in \mathrm{dom}F\to F\left(x\right)=\varnothing$$
25		0ss	$$⊢\varnothing \subseteq B$$
26	24 25	eqsstrdi	$$⊢\neg x\in \mathrm{dom}F\to F\left(x\right)\subseteq B$$
27	23 26	pm2.61i	$$⊢F\left(x\right)\subseteq B$$
28		rsp	$$⊢\forall x\in AB\subseteq C\to \left(x\in A\to B\subseteq C\right)$$
29	28	impcom	$$⊢\left(x\in A\wedge \forall x\in AB\subseteq C\right)\to B\subseteq C$$
30	27 29	sstrid	$$⊢\left(x\in A\wedge \forall x\in AB\subseteq C\right)\to F\left(x\right)\subseteq C$$
31	30	ex	$$⊢x\in A\to \left(\forall x\in AB\subseteq C\to F\left(x\right)\subseteq C\right)$$
32	7 14 17 31	vtoclgaf	$$⊢y\in A\to \left(\forall x\in AB\subseteq C\to F\left(y\right)\subseteq C\right)$$
33	6 32	vtoclga	$$⊢D\in A\to \left(\forall x\in AB\subseteq C\to F\left(D\right)\subseteq C\right)$$
34	33	impcom	$$⊢\left(\forall x\in AB\subseteq C\wedge D\in A\right)\to F\left(D\right)\subseteq C$$
35	3 34	sylan2	$$⊢\left(\forall x\in AB\subseteq C\wedge D\in \mathrm{dom}F\right)\to F\left(D\right)\subseteq C$$
36		ndmfv	$$⊢\neg D\in \mathrm{dom}F\to F\left(D\right)=\varnothing$$
37	36	adantl	$$⊢\left(\forall x\in AB\subseteq C\wedge \neg D\in \mathrm{dom}F\right)\to F\left(D\right)=\varnothing$$
38		0ss	$$⊢\varnothing \subseteq C$$
39	37 38	eqsstrdi	$$⊢\left(\forall x\in AB\subseteq C\wedge \neg D\in \mathrm{dom}F\right)\to F\left(D\right)\subseteq C$$
40	35 39	pm2.61dan	$$⊢\forall x\in AB\subseteq C\to F\left(D\right)\subseteq C$$