Theorem fvmptss2

Description: A mapping always evaluates to a subset of the substituted expression in the mapping, even if this is a proper class, or we are out of the domain. (Contributed by Mario Carneiro, 13-Feb-2015)

	Ref	Expression
Hypotheses	fvmptn.1	$$⊢x=D\to B=C$$
	fvmptn.2	$$⊢F=\left(x\in A⟼B\right)$$
Assertion	fvmptss2	$$⊢F\left(D\right)\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		fvmptn.1	$$⊢x=D\to B=C$$
2		fvmptn.2	$$⊢F=\left(x\in A⟼B\right)$$
3	1	eleq1d	$$⊢x=D\to \left(B\in \mathrm{V}\leftrightarrow C\in \mathrm{V}\right)$$
4	2	dmmpt	$$⊢\mathrm{dom}F=\left\{x\in A|B\in \mathrm{V}\right\}$$
5	3 4	elrab2	$$⊢D\in \mathrm{dom}F\leftrightarrow \left(D\in A\wedge C\in \mathrm{V}\right)$$
6	1 2	fvmptg	$$⊢\left(D\in A\wedge C\in \mathrm{V}\right)\to F\left(D\right)=C$$
7		eqimss	$$⊢F\left(D\right)=C\to F\left(D\right)\subseteq C$$
8	6 7	syl	$$⊢\left(D\in A\wedge C\in \mathrm{V}\right)\to F\left(D\right)\subseteq C$$
9	5 8	sylbi	$$⊢D\in \mathrm{dom}F\to F\left(D\right)\subseteq C$$
10		ndmfv	$$⊢\neg D\in \mathrm{dom}F\to F\left(D\right)=\varnothing$$
11		0ss	$$⊢\varnothing \subseteq C$$
12	10 11	eqsstrdi	$$⊢\neg D\in \mathrm{dom}F\to F\left(D\right)\subseteq C$$
13	9 12	pm2.61i	$$⊢F\left(D\right)\subseteq C$$