Step |
Hyp |
Ref |
Expression |
1 |
|
curry1.1 |
|- G = ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) |
2 |
|
fnfun |
|- ( F Fn ( A X. B ) -> Fun F ) |
3 |
|
2ndconst |
|- ( C e. A -> ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V ) |
4 |
|
dff1o3 |
|- ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V <-> ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -onto-> _V /\ Fun `' ( 2nd |` ( { C } X. _V ) ) ) ) |
5 |
4
|
simprbi |
|- ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V -> Fun `' ( 2nd |` ( { C } X. _V ) ) ) |
6 |
3 5
|
syl |
|- ( C e. A -> Fun `' ( 2nd |` ( { C } X. _V ) ) ) |
7 |
|
funco |
|- ( ( Fun F /\ Fun `' ( 2nd |` ( { C } X. _V ) ) ) -> Fun ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) ) |
8 |
2 6 7
|
syl2an |
|- ( ( F Fn ( A X. B ) /\ C e. A ) -> Fun ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) ) |
9 |
|
dmco |
|- dom ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) = ( `' `' ( 2nd |` ( { C } X. _V ) ) " dom F ) |
10 |
|
fndm |
|- ( F Fn ( A X. B ) -> dom F = ( A X. B ) ) |
11 |
10
|
adantr |
|- ( ( F Fn ( A X. B ) /\ C e. A ) -> dom F = ( A X. B ) ) |
12 |
11
|
imaeq2d |
|- ( ( F Fn ( A X. B ) /\ C e. A ) -> ( `' `' ( 2nd |` ( { C } X. _V ) ) " dom F ) = ( `' `' ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) ) |
13 |
|
imacnvcnv |
|- ( `' `' ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) = ( ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) |
14 |
|
df-ima |
|- ( ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) = ran ( ( 2nd |` ( { C } X. _V ) ) |` ( A X. B ) ) |
15 |
|
resres |
|- ( ( 2nd |` ( { C } X. _V ) ) |` ( A X. B ) ) = ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) ) |
16 |
15
|
rneqi |
|- ran ( ( 2nd |` ( { C } X. _V ) ) |` ( A X. B ) ) = ran ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) ) |
17 |
13 14 16
|
3eqtri |
|- ( `' `' ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) = ran ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) ) |
18 |
|
inxp |
|- ( ( { C } X. _V ) i^i ( A X. B ) ) = ( ( { C } i^i A ) X. ( _V i^i B ) ) |
19 |
|
incom |
|- ( _V i^i B ) = ( B i^i _V ) |
20 |
|
inv1 |
|- ( B i^i _V ) = B |
21 |
19 20
|
eqtri |
|- ( _V i^i B ) = B |
22 |
21
|
xpeq2i |
|- ( ( { C } i^i A ) X. ( _V i^i B ) ) = ( ( { C } i^i A ) X. B ) |
23 |
18 22
|
eqtri |
|- ( ( { C } X. _V ) i^i ( A X. B ) ) = ( ( { C } i^i A ) X. B ) |
24 |
|
snssi |
|- ( C e. A -> { C } C_ A ) |
25 |
|
df-ss |
|- ( { C } C_ A <-> ( { C } i^i A ) = { C } ) |
26 |
24 25
|
sylib |
|- ( C e. A -> ( { C } i^i A ) = { C } ) |
27 |
26
|
xpeq1d |
|- ( C e. A -> ( ( { C } i^i A ) X. B ) = ( { C } X. B ) ) |
28 |
23 27
|
eqtrid |
|- ( C e. A -> ( ( { C } X. _V ) i^i ( A X. B ) ) = ( { C } X. B ) ) |
29 |
28
|
reseq2d |
|- ( C e. A -> ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) ) = ( 2nd |` ( { C } X. B ) ) ) |
30 |
29
|
rneqd |
|- ( C e. A -> ran ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) ) = ran ( 2nd |` ( { C } X. B ) ) ) |
31 |
|
2ndconst |
|- ( C e. A -> ( 2nd |` ( { C } X. B ) ) : ( { C } X. B ) -1-1-onto-> B ) |
32 |
|
f1ofo |
|- ( ( 2nd |` ( { C } X. B ) ) : ( { C } X. B ) -1-1-onto-> B -> ( 2nd |` ( { C } X. B ) ) : ( { C } X. B ) -onto-> B ) |
33 |
|
forn |
|- ( ( 2nd |` ( { C } X. B ) ) : ( { C } X. B ) -onto-> B -> ran ( 2nd |` ( { C } X. B ) ) = B ) |
34 |
31 32 33
|
3syl |
|- ( C e. A -> ran ( 2nd |` ( { C } X. B ) ) = B ) |
35 |
30 34
|
eqtrd |
|- ( C e. A -> ran ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) ) = B ) |
36 |
17 35
|
eqtrid |
|- ( C e. A -> ( `' `' ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) = B ) |
37 |
36
|
adantl |
|- ( ( F Fn ( A X. B ) /\ C e. A ) -> ( `' `' ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) = B ) |
38 |
12 37
|
eqtrd |
|- ( ( F Fn ( A X. B ) /\ C e. A ) -> ( `' `' ( 2nd |` ( { C } X. _V ) ) " dom F ) = B ) |
39 |
9 38
|
eqtrid |
|- ( ( F Fn ( A X. B ) /\ C e. A ) -> dom ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) = B ) |
40 |
1
|
fneq1i |
|- ( G Fn B <-> ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) Fn B ) |
41 |
|
df-fn |
|- ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) Fn B <-> ( Fun ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) /\ dom ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) = B ) ) |
42 |
40 41
|
bitri |
|- ( G Fn B <-> ( Fun ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) /\ dom ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) = B ) ) |
43 |
8 39 42
|
sylanbrc |
|- ( ( F Fn ( A X. B ) /\ C e. A ) -> G Fn B ) |
44 |
|
dffn5 |
|- ( G Fn B <-> G = ( x e. B |-> ( G ` x ) ) ) |
45 |
43 44
|
sylib |
|- ( ( F Fn ( A X. B ) /\ C e. A ) -> G = ( x e. B |-> ( G ` x ) ) ) |
46 |
1
|
fveq1i |
|- ( G ` x ) = ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) ` x ) |
47 |
|
dff1o4 |
|- ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V <-> ( ( 2nd |` ( { C } X. _V ) ) Fn ( { C } X. _V ) /\ `' ( 2nd |` ( { C } X. _V ) ) Fn _V ) ) |
48 |
3 47
|
sylib |
|- ( C e. A -> ( ( 2nd |` ( { C } X. _V ) ) Fn ( { C } X. _V ) /\ `' ( 2nd |` ( { C } X. _V ) ) Fn _V ) ) |
49 |
|
fvco2 |
|- ( ( `' ( 2nd |` ( { C } X. _V ) ) Fn _V /\ x e. _V ) -> ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) ` x ) = ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) ) |
50 |
49
|
elvd |
|- ( `' ( 2nd |` ( { C } X. _V ) ) Fn _V -> ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) ` x ) = ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) ) |
51 |
48 50
|
simpl2im |
|- ( C e. A -> ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) ` x ) = ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) ) |
52 |
51
|
ad2antlr |
|- ( ( ( F Fn ( A X. B ) /\ C e. A ) /\ x e. B ) -> ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) ` x ) = ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) ) |
53 |
46 52
|
eqtrid |
|- ( ( ( F Fn ( A X. B ) /\ C e. A ) /\ x e. B ) -> ( G ` x ) = ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) ) |
54 |
3
|
adantr |
|- ( ( C e. A /\ x e. B ) -> ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V ) |
55 |
|
snidg |
|- ( C e. A -> C e. { C } ) |
56 |
|
vex |
|- x e. _V |
57 |
|
opelxp |
|- ( <. C , x >. e. ( { C } X. _V ) <-> ( C e. { C } /\ x e. _V ) ) |
58 |
55 56 57
|
sylanblrc |
|- ( C e. A -> <. C , x >. e. ( { C } X. _V ) ) |
59 |
58
|
adantr |
|- ( ( C e. A /\ x e. B ) -> <. C , x >. e. ( { C } X. _V ) ) |
60 |
54 59
|
jca |
|- ( ( C e. A /\ x e. B ) -> ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V /\ <. C , x >. e. ( { C } X. _V ) ) ) |
61 |
58
|
fvresd |
|- ( C e. A -> ( ( 2nd |` ( { C } X. _V ) ) ` <. C , x >. ) = ( 2nd ` <. C , x >. ) ) |
62 |
|
op2ndg |
|- ( ( C e. A /\ x e. _V ) -> ( 2nd ` <. C , x >. ) = x ) |
63 |
62
|
elvd |
|- ( C e. A -> ( 2nd ` <. C , x >. ) = x ) |
64 |
61 63
|
eqtrd |
|- ( C e. A -> ( ( 2nd |` ( { C } X. _V ) ) ` <. C , x >. ) = x ) |
65 |
64
|
adantr |
|- ( ( C e. A /\ x e. B ) -> ( ( 2nd |` ( { C } X. _V ) ) ` <. C , x >. ) = x ) |
66 |
|
f1ocnvfv |
|- ( ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V /\ <. C , x >. e. ( { C } X. _V ) ) -> ( ( ( 2nd |` ( { C } X. _V ) ) ` <. C , x >. ) = x -> ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) = <. C , x >. ) ) |
67 |
60 65 66
|
sylc |
|- ( ( C e. A /\ x e. B ) -> ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) = <. C , x >. ) |
68 |
67
|
fveq2d |
|- ( ( C e. A /\ x e. B ) -> ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) = ( F ` <. C , x >. ) ) |
69 |
68
|
adantll |
|- ( ( ( F Fn ( A X. B ) /\ C e. A ) /\ x e. B ) -> ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) = ( F ` <. C , x >. ) ) |
70 |
|
df-ov |
|- ( C F x ) = ( F ` <. C , x >. ) |
71 |
69 70
|
eqtr4di |
|- ( ( ( F Fn ( A X. B ) /\ C e. A ) /\ x e. B ) -> ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) = ( C F x ) ) |
72 |
53 71
|
eqtrd |
|- ( ( ( F Fn ( A X. B ) /\ C e. A ) /\ x e. B ) -> ( G ` x ) = ( C F x ) ) |
73 |
72
|
mpteq2dva |
|- ( ( F Fn ( A X. B ) /\ C e. A ) -> ( x e. B |-> ( G ` x ) ) = ( x e. B |-> ( C F x ) ) ) |
74 |
45 73
|
eqtrd |
|- ( ( F Fn ( A X. B ) /\ C e. A ) -> G = ( x e. B |-> ( C F x ) ) ) |