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