Theorem ovmpos

Description: Value of a function given by the maps-to notation, expressed using explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Hypothesis	ovmpos.3	$$⊢F=\left(x\in C,y\in D⟼R\right)$$
Assertion	ovmpos	$$⊢\left(A\in C\wedge B\in D\wedge ⦋A/x⦌⦋B/y⦌R\in V\right)\to AFB=⦋A/x⦌⦋B/y⦌R$$

Proof

Step	Hyp	Ref	Expression
1		ovmpos.3	$$⊢F=\left(x\in C,y\in D⟼R\right)$$
2		elex	$$⊢⦋A/x⦌⦋B/y⦌R\in V\to ⦋A/x⦌⦋B/y⦌R\in \mathrm{V}$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
6		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋A/x⦌R$$
7	6	nfel1	$$⊢Ⅎx⦋A/x⦌R\in \mathrm{V}$$
8		nfmpo1	$$⊢\underset{\_}{Ⅎ}x\left(x\in C,y\in D⟼R\right)$$
9	1 8	nfcxfr	$$⊢\underset{\_}{Ⅎ}xF$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
11	3 9 10	nfov	$$⊢\underset{\_}{Ⅎ}x\left(AFy\right)$$
12	11 6	nfeq	$$⊢ℲxAFy=⦋A/x⦌R$$
13	7 12	nfim	$$⊢Ⅎx\left(⦋A/x⦌R\in \mathrm{V}\to AFy=⦋A/x⦌R\right)$$
14		nfcsb1v	$$⊢\underset{\_}{Ⅎ}y⦋B/y⦌⦋A/x⦌R$$
15	14	nfel1	$$⊢Ⅎy⦋B/y⦌⦋A/x⦌R\in \mathrm{V}$$
16		nfmpo2	$$⊢\underset{\_}{Ⅎ}y\left(x\in C,y\in D⟼R\right)$$
17	1 16	nfcxfr	$$⊢\underset{\_}{Ⅎ}yF$$
18	4 17 5	nfov	$$⊢\underset{\_}{Ⅎ}y\left(AFB\right)$$
19	18 14	nfeq	$$⊢ℲyAFB=⦋B/y⦌⦋A/x⦌R$$
20	15 19	nfim	$$⊢Ⅎy\left(⦋B/y⦌⦋A/x⦌R\in \mathrm{V}\to AFB=⦋B/y⦌⦋A/x⦌R\right)$$
21		csbeq1a	$$⊢x=A\to R=⦋A/x⦌R$$
22	21	eleq1d	$$⊢x=A\to \left(R\in \mathrm{V}\leftrightarrow ⦋A/x⦌R\in \mathrm{V}\right)$$
23		oveq1	$$⊢x=A\to xFy=AFy$$
24	23 21	eqeq12d	$$⊢x=A\to \left(xFy=R\leftrightarrow AFy=⦋A/x⦌R\right)$$
25	22 24	imbi12d	$$⊢x=A\to \left(\left(R\in \mathrm{V}\to xFy=R\right)\leftrightarrow \left(⦋A/x⦌R\in \mathrm{V}\to AFy=⦋A/x⦌R\right)\right)$$
26		csbeq1a	$$⊢y=B\to ⦋A/x⦌R=⦋B/y⦌⦋A/x⦌R$$
27	26	eleq1d	$$⊢y=B\to \left(⦋A/x⦌R\in \mathrm{V}\leftrightarrow ⦋B/y⦌⦋A/x⦌R\in \mathrm{V}\right)$$
28		oveq2	$$⊢y=B\to AFy=AFB$$
29	28 26	eqeq12d	$$⊢y=B\to \left(AFy=⦋A/x⦌R\leftrightarrow AFB=⦋B/y⦌⦋A/x⦌R\right)$$
30	27 29	imbi12d	$$⊢y=B\to \left(\left(⦋A/x⦌R\in \mathrm{V}\to AFy=⦋A/x⦌R\right)\leftrightarrow \left(⦋B/y⦌⦋A/x⦌R\in \mathrm{V}\to AFB=⦋B/y⦌⦋A/x⦌R\right)\right)$$
31	1	ovmpt4g	$$⊢\left(x\in C\wedge y\in D\wedge R\in \mathrm{V}\right)\to xFy=R$$
32	31	3expia	$$⊢\left(x\in C\wedge y\in D\right)\to \left(R\in \mathrm{V}\to xFy=R\right)$$
33	3 4 5 13 20 25 30 32	vtocl2gaf	$$⊢\left(A\in C\wedge B\in D\right)\to \left(⦋B/y⦌⦋A/x⦌R\in \mathrm{V}\to AFB=⦋B/y⦌⦋A/x⦌R\right)$$
34		csbcom	$$⊢⦋A/x⦌⦋B/y⦌R=⦋B/y⦌⦋A/x⦌R$$
35	34	eleq1i	$$⊢⦋A/x⦌⦋B/y⦌R\in \mathrm{V}\leftrightarrow ⦋B/y⦌⦋A/x⦌R\in \mathrm{V}$$
36	34	eqeq2i	$$⊢AFB=⦋A/x⦌⦋B/y⦌R\leftrightarrow AFB=⦋B/y⦌⦋A/x⦌R$$
37	33 35 36	3imtr4g	$$⊢\left(A\in C\wedge B\in D\right)\to \left(⦋A/x⦌⦋B/y⦌R\in \mathrm{V}\to AFB=⦋A/x⦌⦋B/y⦌R\right)$$
38	2 37	syl5	$$⊢\left(A\in C\wedge B\in D\right)\to \left(⦋A/x⦌⦋B/y⦌R\in V\to AFB=⦋A/x⦌⦋B/y⦌R\right)$$
39	38	3impia	$$⊢\left(A\in C\wedge B\in D\wedge ⦋A/x⦌⦋B/y⦌R\in V\right)\to AFB=⦋A/x⦌⦋B/y⦌R$$