Metamath Proof Explorer

Theorem dmmpossx

Description: The domain of a mapping is a subset of its base class. (Contributed by Mario Carneiro, 9-Feb-2015)

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

Proof

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