Theorem dfmpo

Description: Alternate definition for the maps-to notation df-mpo (although it requires that C be a set). (Contributed by NM, 19-Dec-2008) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypothesis	dfmpo.1	$$⊢C\in \mathrm{V}$$
Assertion	dfmpo	$$⊢\left(x\in A,y\in B⟼C\right)=\bigcup _{x\in A}\bigcup _{y\in B}\left\{⟨⟨x,y⟩,C⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfmpo.1	$$⊢C\in \mathrm{V}$$
2		mpompts	$$⊢\left(x\in A,y\in B⟼C\right)=\left(w\in \left(A\times B\right)⟼⦋1^{st}\left(w\right)/x⦌⦋2^{nd}\left(w\right)/y⦌C\right)$$
3	1	csbex	$$⊢⦋2^{nd}\left(w\right)/y⦌C\in \mathrm{V}$$
4	3	csbex	$$⊢⦋1^{st}\left(w\right)/x⦌⦋2^{nd}\left(w\right)/y⦌C\in \mathrm{V}$$
5	4	dfmpt	$$⊢\left(w\in \left(A\times B\right)⟼⦋1^{st}\left(w\right)/x⦌⦋2^{nd}\left(w\right)/y⦌C\right)=\bigcup _{w\in A\times B}\left\{⟨w,⦋1^{st}\left(w\right)/x⦌⦋2^{nd}\left(w\right)/y⦌C⟩\right\}$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}xw$$
7		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋1^{st}\left(w\right)/x⦌⦋2^{nd}\left(w\right)/y⦌C$$
8	6 7	nfop	$$⊢\underset{\_}{Ⅎ}x⟨w,⦋1^{st}\left(w\right)/x⦌⦋2^{nd}\left(w\right)/y⦌C⟩$$
9	8	nfsn	$$⊢\underset{\_}{Ⅎ}x\left\{⟨w,⦋1^{st}\left(w\right)/x⦌⦋2^{nd}\left(w\right)/y⦌C⟩\right\}$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}yw$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}y{1}^{st}\left(w\right)$$
12		nfcsb1v	$$⊢\underset{\_}{Ⅎ}y⦋2^{nd}\left(w\right)/y⦌C$$
13	11 12	nfcsbw	$$⊢\underset{\_}{Ⅎ}y⦋1^{st}\left(w\right)/x⦌⦋2^{nd}\left(w\right)/y⦌C$$
14	10 13	nfop	$$⊢\underset{\_}{Ⅎ}y⟨w,⦋1^{st}\left(w\right)/x⦌⦋2^{nd}\left(w\right)/y⦌C⟩$$
15	14	nfsn	$$⊢\underset{\_}{Ⅎ}y\left\{⟨w,⦋1^{st}\left(w\right)/x⦌⦋2^{nd}\left(w\right)/y⦌C⟩\right\}$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}w\left\{⟨⟨x,y⟩,C⟩\right\}$$
17		id	$$⊢w=⟨x,y⟩\to w=⟨x,y⟩$$
18		csbopeq1a	$$⊢w=⟨x,y⟩\to ⦋1^{st}\left(w\right)/x⦌⦋2^{nd}\left(w\right)/y⦌C=C$$
19	17 18	opeq12d	$$⊢w=⟨x,y⟩\to ⟨w,⦋1^{st}\left(w\right)/x⦌⦋2^{nd}\left(w\right)/y⦌C⟩=⟨⟨x,y⟩,C⟩$$
20	19	sneqd	$$⊢w=⟨x,y⟩\to \left\{⟨w,⦋1^{st}\left(w\right)/x⦌⦋2^{nd}\left(w\right)/y⦌C⟩\right\}=\left\{⟨⟨x,y⟩,C⟩\right\}$$
21	9 15 16 20	iunxpf	$$⊢\bigcup _{w\in A\times B}\left\{⟨w,⦋1^{st}\left(w\right)/x⦌⦋2^{nd}\left(w\right)/y⦌C⟩\right\}=\bigcup _{x\in A}\bigcup _{y\in B}\left\{⟨⟨x,y⟩,C⟩\right\}$$
22	2 5 21	3eqtri	$$⊢\left(x\in A,y\in B⟼C\right)=\bigcup _{x\in A}\bigcup _{y\in B}\left\{⟨⟨x,y⟩,C⟩\right\}$$