Theorem ovmptss

Description: If all the values of the mapping are subsets of a class X , then so is any evaluation of the mapping. (Contributed by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Hypothesis	ovmptss.1	$$⊢F=\left(x\in A,y\in B⟼C\right)$$
Assertion	ovmptss	$$⊢\forall x\in A\forall y\in BC\subseteq X\to EFG\subseteq X$$

Proof

Step	Hyp	Ref	Expression
1		ovmptss.1	$$⊢F=\left(x\in A,y\in B⟼C\right)$$
2		mpomptsx	$$⊢\left(x\in A,y\in B⟼C\right)=\left(z\in \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)⟼⦋1^{st}\left(z\right)/x⦌⦋2^{nd}\left(z\right)/y⦌C\right)$$
3	1 2	eqtri	$$⊢F=\left(z\in \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)⟼⦋1^{st}\left(z\right)/x⦌⦋2^{nd}\left(z\right)/y⦌C\right)$$
4	3	fvmptss	$$⊢\forall z\in \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)⦋1^{st}\left(z\right)/x⦌⦋2^{nd}\left(z\right)/y⦌C\subseteq X\to F\left(⟨E,G⟩\right)\subseteq X$$
5		vex	$$⊢u\in \mathrm{V}$$
6		vex	$$⊢v\in \mathrm{V}$$
7	5 6	op1std	$$⊢z=⟨u,v⟩\to 1^{st}\left(z\right)=u$$
8	7	csbeq1d	$$⊢z=⟨u,v⟩\to ⦋1^{st}\left(z\right)/x⦌⦋2^{nd}\left(z\right)/y⦌C=⦋u/x⦌⦋2^{nd}\left(z\right)/y⦌C$$
9	5 6	op2ndd	$$⊢z=⟨u,v⟩\to 2^{nd}\left(z\right)=v$$
10	9	csbeq1d	$$⊢z=⟨u,v⟩\to ⦋2^{nd}\left(z\right)/y⦌C=⦋v/y⦌C$$
11	10	csbeq2dv	$$⊢z=⟨u,v⟩\to ⦋u/x⦌⦋2^{nd}\left(z\right)/y⦌C=⦋u/x⦌⦋v/y⦌C$$
12	8 11	eqtrd	$$⊢z=⟨u,v⟩\to ⦋1^{st}\left(z\right)/x⦌⦋2^{nd}\left(z\right)/y⦌C=⦋u/x⦌⦋v/y⦌C$$
13	12	sseq1d	$$⊢z=⟨u,v⟩\to \left(⦋1^{st}\left(z\right)/x⦌⦋2^{nd}\left(z\right)/y⦌C\subseteq X\leftrightarrow ⦋u/x⦌⦋v/y⦌C\subseteq X\right)$$
14	13	raliunxp	$$⊢\forall z\in \bigcup _{u\in A}\left(\left\{u\right\}\times ⦋u/x⦌B\right)⦋1^{st}\left(z\right)/x⦌⦋2^{nd}\left(z\right)/y⦌C\subseteq X\leftrightarrow \forall u\in A\forall v\in ⦋u/x⦌B⦋u/x⦌⦋v/y⦌C\subseteq X$$
15		nfcv	$$⊢\underset{\_}{Ⅎ}u\left(\left\{x\right\}\times B\right)$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}x\left\{u\right\}$$
17		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋u/x⦌B$$
18	16 17	nfxp	$$⊢\underset{\_}{Ⅎ}x\left(\left\{u\right\}\times ⦋u/x⦌B\right)$$
19		sneq	$$⊢x=u\to \left\{x\right\}=\left\{u\right\}$$
20		csbeq1a	$$⊢x=u\to B=⦋u/x⦌B$$
21	19 20	xpeq12d	$$⊢x=u\to \left\{x\right\}\times B=\left\{u\right\}\times ⦋u/x⦌B$$
22	15 18 21	cbviun	$$⊢\bigcup _{x\in A}\left(\left\{x\right\}\times B\right)=\bigcup _{u\in A}\left(\left\{u\right\}\times ⦋u/x⦌B\right)$$
23	22	raleqi	$$⊢\forall z\in \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)⦋1^{st}\left(z\right)/x⦌⦋2^{nd}\left(z\right)/y⦌C\subseteq X\leftrightarrow \forall z\in \bigcup _{u\in A}\left(\left\{u\right\}\times ⦋u/x⦌B\right)⦋1^{st}\left(z\right)/x⦌⦋2^{nd}\left(z\right)/y⦌C\subseteq X$$
24		nfv	$$⊢Ⅎu\forall y\in BC\subseteq X$$
25		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋u/x⦌⦋v/y⦌C$$
26		nfcv	$$⊢\underset{\_}{Ⅎ}xX$$
27	25 26	nfss	$$⊢Ⅎx⦋u/x⦌⦋v/y⦌C\subseteq X$$
28	17 27	nfralw	$$⊢Ⅎx\forall v\in ⦋u/x⦌B⦋u/x⦌⦋v/y⦌C\subseteq X$$
29		nfv	$$⊢ℲvC\subseteq X$$
30		nfcsb1v	$$⊢\underset{\_}{Ⅎ}y⦋v/y⦌C$$
31		nfcv	$$⊢\underset{\_}{Ⅎ}yX$$
32	30 31	nfss	$$⊢Ⅎy⦋v/y⦌C\subseteq X$$
33		csbeq1a	$$⊢y=v\to C=⦋v/y⦌C$$
34	33	sseq1d	$$⊢y=v\to \left(C\subseteq X\leftrightarrow ⦋v/y⦌C\subseteq X\right)$$
35	29 32 34	cbvralw	$$⊢\forall y\in BC\subseteq X\leftrightarrow \forall v\in B⦋v/y⦌C\subseteq X$$
36		csbeq1a	$$⊢x=u\to ⦋v/y⦌C=⦋u/x⦌⦋v/y⦌C$$
37	36	sseq1d	$$⊢x=u\to \left(⦋v/y⦌C\subseteq X\leftrightarrow ⦋u/x⦌⦋v/y⦌C\subseteq X\right)$$
38	20 37	raleqbidv	$$⊢x=u\to \left(\forall v\in B⦋v/y⦌C\subseteq X\leftrightarrow \forall v\in ⦋u/x⦌B⦋u/x⦌⦋v/y⦌C\subseteq X\right)$$
39	35 38	syl5bb	$$⊢x=u\to \left(\forall y\in BC\subseteq X\leftrightarrow \forall v\in ⦋u/x⦌B⦋u/x⦌⦋v/y⦌C\subseteq X\right)$$
40	24 28 39	cbvralw	$$⊢\forall x\in A\forall y\in BC\subseteq X\leftrightarrow \forall u\in A\forall v\in ⦋u/x⦌B⦋u/x⦌⦋v/y⦌C\subseteq X$$
41	14 23 40	3bitr4ri	$$⊢\forall x\in A\forall y\in BC\subseteq X\leftrightarrow \forall z\in \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)⦋1^{st}\left(z\right)/x⦌⦋2^{nd}\left(z\right)/y⦌C\subseteq X$$
42		df-ov	$$⊢EFG=F\left(⟨E,G⟩\right)$$
43	42	sseq1i	$$⊢EFG\subseteq X\leftrightarrow F\left(⟨E,G⟩\right)\subseteq X$$
44	4 41 43	3imtr4i	$$⊢\forall x\in A\forall y\in BC\subseteq X\to EFG\subseteq X$$