# 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 )`