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 )