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 e. _V
Assertion	dfmpo	|- ( x e. A , y e. B |-> C ) = U_ x e. A U_ y e. B { <. <. x , y >. , C >. }

Proof

Step	Hyp	Ref	Expression
1		dfmpo.1	|- C e. _V
2		mpompts	|- ( x e. A , y e. B |-> C ) = ( w e. ( A X. B ) |-> [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C )
3	1	csbex	|- [_ ( 2nd ` w ) / y ]_ C e. _V
4	3	csbex	|- [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C e. _V
5	4	dfmpt	|- ( w e. ( A X. B ) |-> [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C ) = U_ w e. ( A X. B ) { <. w , [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C >. }
6		nfcv	|- F/_ x w
7		nfcsb1v	|- F/_ x [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C
8	6 7	nfop	|- F/_ x <. w , [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C >.
9	8	nfsn	|- F/_ x { <. w , [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C >. }
10		nfcv	|- F/_ y w
11		nfcv	|- F/_ y ( 1st ` w )
12		nfcsb1v	|- F/_ y [_ ( 2nd ` w ) / y ]_ C
13	11 12	nfcsbw	|- F/_ y [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C
14	10 13	nfop	|- F/_ y <. w , [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C >.
15	14	nfsn	|- F/_ y { <. w , [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C >. }
16		nfcv	|- F/_ w { <. <. x , y >. , C >. }
17		id	|- ( w = <. x , y >. -> w = <. x , y >. )
18		csbopeq1a	|- ( w = <. x , y >. -> [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C = C )
19	17 18	opeq12d	|- ( w = <. x , y >. -> <. w , [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C >. = <. <. x , y >. , C >. )
20	19	sneqd	|- ( w = <. x , y >. -> { <. w , [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C >. } = { <. <. x , y >. , C >. } )
21	9 15 16 20	iunxpf	|- U_ w e. ( A X. B ) { <. w , [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C >. } = U_ x e. A U_ y e. B { <. <. x , y >. , C >. }
22	2 5 21	3eqtri	|- ( x e. A , y e. B |-> C ) = U_ x e. A U_ y e. B { <. <. x , y >. , C >. }