Metamath Proof Explorer

Theorem dmmpossx2

Description: The domain of a mapping is a subset of its base classes expressed as union of Cartesian products over its second component, analogous to dmmpossx . (Contributed by AV, 30-Mar-2019)

Ref Expression
Hypothesis dmmpossx2.1 
|- F = ( x e. A , y e. B |-> C )
Assertion dmmpossx2 
|- dom F C_ U_ y e. B ( A X. { y } )

Proof

Step Hyp Ref Expression
1 dmmpossx2.1 
 |-  F = ( x e. A , y e. B |-> C )
2 nfcv 
 |-  F/_ u A
3 nfcsb1v 
 |-  F/_ y [_ u / y ]_ A
4 nfcv 
 |-  F/_ u C
5 nfcv 
 |-  F/_ v C
6 nfcv 
 |-  F/_ x u
7 nfcsb1v 
 |-  F/_ x [_ v / x ]_ C
8 6 7 nfcsbw 
 |-  F/_ x [_ u / y ]_ [_ v / x ]_ C
9 nfcsb1v 
 |-  F/_ y [_ u / y ]_ [_ v / x ]_ C
10 csbeq1a 
 |-  ( y = u -> A = [_ u / y ]_ A )
11 csbeq1a 
 |-  ( x = v -> C = [_ v / x ]_ C )
12 csbeq1a 
 |-  ( y = u -> [_ v / x ]_ C = [_ u / y ]_ [_ v / x ]_ C )
13 11 12 sylan9eqr 
 |-  ( ( y = u /\ x = v ) -> C = [_ u / y ]_ [_ v / x ]_ C )
14 2 3 4 5 8 9 10 13 cbvmpox2 
 |-  ( x e. A , y e. B |-> C ) = ( v e. [_ u / y ]_ A , u e. B |-> [_ u / y ]_ [_ v / x ]_ C )
15 vex 
 |-  v e. _V
16 vex 
 |-  u e. _V
17 15 16 op2ndd 
 |-  ( t = <. v , u >. -> ( 2nd ` t ) = u )
18 17 csbeq1d 
 |-  ( t = <. v , u >. -> [_ ( 2nd ` t ) / y ]_ [_ ( 1st ` t ) / x ]_ C = [_ u / y ]_ [_ ( 1st ` t ) / x ]_ C )
19 15 16 op1std 
 |-  ( t = <. v , u >. -> ( 1st ` t ) = v )
20 19 csbeq1d 
 |-  ( t = <. v , u >. -> [_ ( 1st ` t ) / x ]_ C = [_ v / x ]_ C )
21 20 csbeq2dv 
 |-  ( t = <. v , u >. -> [_ u / y ]_ [_ ( 1st ` t ) / x ]_ C = [_ u / y ]_ [_ v / x ]_ C )
22 18 21 eqtrd 
 |-  ( t = <. v , u >. -> [_ ( 2nd ` t ) / y ]_ [_ ( 1st ` t ) / x ]_ C = [_ u / y ]_ [_ v / x ]_ C )
23 22 mpomptx2 
 |-  ( t e. U_ u e. B ( [_ u / y ]_ A X. { u } ) |-> [_ ( 2nd ` t ) / y ]_ [_ ( 1st ` t ) / x ]_ C ) = ( v e. [_ u / y ]_ A , u e. B |-> [_ u / y ]_ [_ v / x ]_ C )
24 14 1 23 3eqtr4i 
 |-  F = ( t e. U_ u e. B ( [_ u / y ]_ A X. { u } ) |-> [_ ( 2nd ` t ) / y ]_ [_ ( 1st ` t ) / x ]_ C )
25 24 dmmptss 
 |-  dom F C_ U_ u e. B ( [_ u / y ]_ A X. { u } )
26 nfcv 
 |-  F/_ u ( A X. { y } )
27 nfcv 
 |-  F/_ y { u }
28 3 27 nfxp 
 |-  F/_ y ( [_ u / y ]_ A X. { u } )
29 sneq 
 |-  ( y = u -> { y } = { u } )
30 10 29 xpeq12d 
 |-  ( y = u -> ( A X. { y } ) = ( [_ u / y ]_ A X. { u } ) )
31 26 28 30 cbviun 
 |-  U_ y e. B ( A X. { y } ) = U_ u e. B ( [_ u / y ]_ A X. { u } )
32 25 31 sseqtrri 
 |-  dom F C_ U_ y e. B ( A X. { y } )