Step |
Hyp |
Ref |
Expression |
1 |
|
ofpreima.1 |
|- ( ph -> F : A --> B ) |
2 |
|
ofpreima.2 |
|- ( ph -> G : A --> C ) |
3 |
|
ofpreima.3 |
|- ( ph -> A e. V ) |
4 |
|
ofpreima.4 |
|- ( ph -> R Fn ( B X. C ) ) |
5 |
|
nfmpt1 |
|- F/_ s ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) |
6 |
|
eqidd |
|- ( ph -> ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) = ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) ) |
7 |
|
fnov |
|- ( R Fn ( B X. C ) <-> R = ( x e. B , y e. C |-> ( x R y ) ) ) |
8 |
4 7
|
sylib |
|- ( ph -> R = ( x e. B , y e. C |-> ( x R y ) ) ) |
9 |
5 1 2 3 6 8
|
ofoprabco |
|- ( ph -> ( F oF R G ) = ( R o. ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) ) ) |
10 |
9
|
cnveqd |
|- ( ph -> `' ( F oF R G ) = `' ( R o. ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) ) ) |
11 |
|
cnvco |
|- `' ( R o. ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) ) = ( `' ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) o. `' R ) |
12 |
10 11
|
eqtrdi |
|- ( ph -> `' ( F oF R G ) = ( `' ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) o. `' R ) ) |
13 |
12
|
imaeq1d |
|- ( ph -> ( `' ( F oF R G ) " D ) = ( ( `' ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) o. `' R ) " D ) ) |
14 |
|
imaco |
|- ( ( `' ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) o. `' R ) " D ) = ( `' ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) " ( `' R " D ) ) |
15 |
13 14
|
eqtrdi |
|- ( ph -> ( `' ( F oF R G ) " D ) = ( `' ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) " ( `' R " D ) ) ) |
16 |
|
dfima2 |
|- ( `' ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) " ( `' R " D ) ) = { q | E. p e. ( `' R " D ) p `' ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) q } |
17 |
|
vex |
|- p e. _V |
18 |
|
vex |
|- q e. _V |
19 |
17 18
|
brcnv |
|- ( p `' ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) q <-> q ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) p ) |
20 |
|
funmpt |
|- Fun ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) |
21 |
|
funbrfv2b |
|- ( Fun ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) -> ( q ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) p <-> ( q e. dom ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) /\ ( ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) ` q ) = p ) ) ) |
22 |
20 21
|
ax-mp |
|- ( q ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) p <-> ( q e. dom ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) /\ ( ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) ` q ) = p ) ) |
23 |
|
opex |
|- <. ( F ` s ) , ( G ` s ) >. e. _V |
24 |
|
eqid |
|- ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) = ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) |
25 |
23 24
|
dmmpti |
|- dom ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) = A |
26 |
25
|
eleq2i |
|- ( q e. dom ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) <-> q e. A ) |
27 |
26
|
anbi1i |
|- ( ( q e. dom ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) /\ ( ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) ` q ) = p ) <-> ( q e. A /\ ( ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) ` q ) = p ) ) |
28 |
22 27
|
bitri |
|- ( q ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) p <-> ( q e. A /\ ( ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) ` q ) = p ) ) |
29 |
|
fveq2 |
|- ( s = q -> ( F ` s ) = ( F ` q ) ) |
30 |
|
fveq2 |
|- ( s = q -> ( G ` s ) = ( G ` q ) ) |
31 |
29 30
|
opeq12d |
|- ( s = q -> <. ( F ` s ) , ( G ` s ) >. = <. ( F ` q ) , ( G ` q ) >. ) |
32 |
|
opex |
|- <. ( F ` q ) , ( G ` q ) >. e. _V |
33 |
31 24 32
|
fvmpt |
|- ( q e. A -> ( ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) ` q ) = <. ( F ` q ) , ( G ` q ) >. ) |
34 |
33
|
eqeq1d |
|- ( q e. A -> ( ( ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) ` q ) = p <-> <. ( F ` q ) , ( G ` q ) >. = p ) ) |
35 |
34
|
pm5.32i |
|- ( ( q e. A /\ ( ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) ` q ) = p ) <-> ( q e. A /\ <. ( F ` q ) , ( G ` q ) >. = p ) ) |
36 |
19 28 35
|
3bitri |
|- ( p `' ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) q <-> ( q e. A /\ <. ( F ` q ) , ( G ` q ) >. = p ) ) |
37 |
36
|
rexbii |
|- ( E. p e. ( `' R " D ) p `' ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) q <-> E. p e. ( `' R " D ) ( q e. A /\ <. ( F ` q ) , ( G ` q ) >. = p ) ) |
38 |
37
|
abbii |
|- { q | E. p e. ( `' R " D ) p `' ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) q } = { q | E. p e. ( `' R " D ) ( q e. A /\ <. ( F ` q ) , ( G ` q ) >. = p ) } |
39 |
|
nfv |
|- F/ q ph |
40 |
|
nfab1 |
|- F/_ q { q | E. p e. ( `' R " D ) ( q e. A /\ <. ( F ` q ) , ( G ` q ) >. = p ) } |
41 |
|
nfcv |
|- F/_ q U_ p e. ( `' R " D ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) |
42 |
|
eliun |
|- ( q e. U_ p e. ( `' R " D ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) <-> E. p e. ( `' R " D ) q e. ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) |
43 |
|
ffn |
|- ( F : A --> B -> F Fn A ) |
44 |
|
fniniseg |
|- ( F Fn A -> ( q e. ( `' F " { ( 1st ` p ) } ) <-> ( q e. A /\ ( F ` q ) = ( 1st ` p ) ) ) ) |
45 |
1 43 44
|
3syl |
|- ( ph -> ( q e. ( `' F " { ( 1st ` p ) } ) <-> ( q e. A /\ ( F ` q ) = ( 1st ` p ) ) ) ) |
46 |
|
ffn |
|- ( G : A --> C -> G Fn A ) |
47 |
|
fniniseg |
|- ( G Fn A -> ( q e. ( `' G " { ( 2nd ` p ) } ) <-> ( q e. A /\ ( G ` q ) = ( 2nd ` p ) ) ) ) |
48 |
2 46 47
|
3syl |
|- ( ph -> ( q e. ( `' G " { ( 2nd ` p ) } ) <-> ( q e. A /\ ( G ` q ) = ( 2nd ` p ) ) ) ) |
49 |
45 48
|
anbi12d |
|- ( ph -> ( ( q e. ( `' F " { ( 1st ` p ) } ) /\ q e. ( `' G " { ( 2nd ` p ) } ) ) <-> ( ( q e. A /\ ( F ` q ) = ( 1st ` p ) ) /\ ( q e. A /\ ( G ` q ) = ( 2nd ` p ) ) ) ) ) |
50 |
|
elin |
|- ( q e. ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) <-> ( q e. ( `' F " { ( 1st ` p ) } ) /\ q e. ( `' G " { ( 2nd ` p ) } ) ) ) |
51 |
|
anandi |
|- ( ( q e. A /\ ( ( F ` q ) = ( 1st ` p ) /\ ( G ` q ) = ( 2nd ` p ) ) ) <-> ( ( q e. A /\ ( F ` q ) = ( 1st ` p ) ) /\ ( q e. A /\ ( G ` q ) = ( 2nd ` p ) ) ) ) |
52 |
49 50 51
|
3bitr4g |
|- ( ph -> ( q e. ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) <-> ( q e. A /\ ( ( F ` q ) = ( 1st ` p ) /\ ( G ` q ) = ( 2nd ` p ) ) ) ) ) |
53 |
52
|
adantr |
|- ( ( ph /\ p e. ( `' R " D ) ) -> ( q e. ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) <-> ( q e. A /\ ( ( F ` q ) = ( 1st ` p ) /\ ( G ` q ) = ( 2nd ` p ) ) ) ) ) |
54 |
|
cnvimass |
|- ( `' R " D ) C_ dom R |
55 |
4
|
fndmd |
|- ( ph -> dom R = ( B X. C ) ) |
56 |
54 55
|
sseqtrid |
|- ( ph -> ( `' R " D ) C_ ( B X. C ) ) |
57 |
56
|
sselda |
|- ( ( ph /\ p e. ( `' R " D ) ) -> p e. ( B X. C ) ) |
58 |
|
1st2nd2 |
|- ( p e. ( B X. C ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. ) |
59 |
|
eqeq2 |
|- ( p = <. ( 1st ` p ) , ( 2nd ` p ) >. -> ( <. ( F ` q ) , ( G ` q ) >. = p <-> <. ( F ` q ) , ( G ` q ) >. = <. ( 1st ` p ) , ( 2nd ` p ) >. ) ) |
60 |
57 58 59
|
3syl |
|- ( ( ph /\ p e. ( `' R " D ) ) -> ( <. ( F ` q ) , ( G ` q ) >. = p <-> <. ( F ` q ) , ( G ` q ) >. = <. ( 1st ` p ) , ( 2nd ` p ) >. ) ) |
61 |
|
fvex |
|- ( F ` q ) e. _V |
62 |
|
fvex |
|- ( G ` q ) e. _V |
63 |
61 62
|
opth |
|- ( <. ( F ` q ) , ( G ` q ) >. = <. ( 1st ` p ) , ( 2nd ` p ) >. <-> ( ( F ` q ) = ( 1st ` p ) /\ ( G ` q ) = ( 2nd ` p ) ) ) |
64 |
60 63
|
bitrdi |
|- ( ( ph /\ p e. ( `' R " D ) ) -> ( <. ( F ` q ) , ( G ` q ) >. = p <-> ( ( F ` q ) = ( 1st ` p ) /\ ( G ` q ) = ( 2nd ` p ) ) ) ) |
65 |
64
|
anbi2d |
|- ( ( ph /\ p e. ( `' R " D ) ) -> ( ( q e. A /\ <. ( F ` q ) , ( G ` q ) >. = p ) <-> ( q e. A /\ ( ( F ` q ) = ( 1st ` p ) /\ ( G ` q ) = ( 2nd ` p ) ) ) ) ) |
66 |
53 65
|
bitr4d |
|- ( ( ph /\ p e. ( `' R " D ) ) -> ( q e. ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) <-> ( q e. A /\ <. ( F ` q ) , ( G ` q ) >. = p ) ) ) |
67 |
66
|
rexbidva |
|- ( ph -> ( E. p e. ( `' R " D ) q e. ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) <-> E. p e. ( `' R " D ) ( q e. A /\ <. ( F ` q ) , ( G ` q ) >. = p ) ) ) |
68 |
|
abid |
|- ( q e. { q | E. p e. ( `' R " D ) ( q e. A /\ <. ( F ` q ) , ( G ` q ) >. = p ) } <-> E. p e. ( `' R " D ) ( q e. A /\ <. ( F ` q ) , ( G ` q ) >. = p ) ) |
69 |
67 68
|
bitr4di |
|- ( ph -> ( E. p e. ( `' R " D ) q e. ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) <-> q e. { q | E. p e. ( `' R " D ) ( q e. A /\ <. ( F ` q ) , ( G ` q ) >. = p ) } ) ) |
70 |
42 69
|
bitr2id |
|- ( ph -> ( q e. { q | E. p e. ( `' R " D ) ( q e. A /\ <. ( F ` q ) , ( G ` q ) >. = p ) } <-> q e. U_ p e. ( `' R " D ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) ) |
71 |
39 40 41 70
|
eqrd |
|- ( ph -> { q | E. p e. ( `' R " D ) ( q e. A /\ <. ( F ` q ) , ( G ` q ) >. = p ) } = U_ p e. ( `' R " D ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) |
72 |
38 71
|
syl5eq |
|- ( ph -> { q | E. p e. ( `' R " D ) p `' ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) q } = U_ p e. ( `' R " D ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) |
73 |
16 72
|
syl5eq |
|- ( ph -> ( `' ( s e. A |-> <. ( F ` s ) , ( G ` s ) >. ) " ( `' R " D ) ) = U_ p e. ( `' R " D ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) |
74 |
15 73
|
eqtrd |
|- ( ph -> ( `' ( F oF R G ) " D ) = U_ p e. ( `' R " D ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) |