This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 >. }