Theorem mpomptsx

Description: Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢u\in \mathrm{V}$$
2		vex	$$⊢v\in \mathrm{V}$$
3	1 2	op1std	$$⊢z=⟨u,v⟩\to 1^{st}\left(z\right)=u$$
4	3	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$$
5	1 2	op2ndd	$$⊢z=⟨u,v⟩\to 2^{nd}\left(z\right)=v$$
6	5	csbeq1d	$$⊢z=⟨u,v⟩\to ⦋2^{nd}\left(z\right)/y⦌C=⦋v/y⦌C$$
7	6	csbeq2dv	$$⊢z=⟨u,v⟩\to ⦋u/x⦌⦋2^{nd}\left(z\right)/y⦌C=⦋u/x⦌⦋v/y⦌C$$
8	4 7	eqtrd	$$⊢z=⟨u,v⟩\to ⦋1^{st}\left(z\right)/x⦌⦋2^{nd}\left(z\right)/y⦌C=⦋u/x⦌⦋v/y⦌C$$
9	8	mpomptx	$$⊢\left(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\right)=\left(u\in A,v\in ⦋u/x⦌B⟼⦋u/x⦌⦋v/y⦌C\right)$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}u\left(\left\{x\right\}\times B\right)$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}x\left\{u\right\}$$
12		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋u/x⦌B$$
13	11 12	nfxp	$$⊢\underset{\_}{Ⅎ}x\left(\left\{u\right\}\times ⦋u/x⦌B\right)$$
14		sneq	$$⊢x=u\to \left\{x\right\}=\left\{u\right\}$$
15		csbeq1a	$$⊢x=u\to B=⦋u/x⦌B$$
16	14 15	xpeq12d	$$⊢x=u\to \left\{x\right\}\times B=\left\{u\right\}\times ⦋u/x⦌B$$
17	10 13 16	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)$$
18	17	mpteq1i	$$⊢\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)=\left(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\right)$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}uB$$
20		nfcv	$$⊢\underset{\_}{Ⅎ}uC$$
21		nfcv	$$⊢\underset{\_}{Ⅎ}vC$$
22		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋u/x⦌⦋v/y⦌C$$
23		nfcv	$$⊢\underset{\_}{Ⅎ}yu$$
24		nfcsb1v	$$⊢\underset{\_}{Ⅎ}y⦋v/y⦌C$$
25	23 24	nfcsbw	$$⊢\underset{\_}{Ⅎ}y⦋u/x⦌⦋v/y⦌C$$
26		csbeq1a	$$⊢y=v\to C=⦋v/y⦌C$$
27		csbeq1a	$$⊢x=u\to ⦋v/y⦌C=⦋u/x⦌⦋v/y⦌C$$
28	26 27	sylan9eqr	$$⊢\left(x=u\wedge y=v\right)\to C=⦋u/x⦌⦋v/y⦌C$$
29	19 12 20 21 22 25 15 28	cbvmpox	$$⊢\left(x\in A,y\in B⟼C\right)=\left(u\in A,v\in ⦋u/x⦌B⟼⦋u/x⦌⦋v/y⦌C\right)$$
30	9 18 29	3eqtr4ri	$$⊢\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)$$