Metamath Proof Explorer

Theorem ofpreima

Description: Express the preimage of a function operation as a union of preimages. (Contributed by Thierry Arnoux, 8-Mar-2018)

Ref Expression
Hypotheses ofpreima.1 
|- ( ph -> F : A --> B )
ofpreima.2 
|- ( ph -> G : A --> C )
ofpreima.3 
|- ( ph -> A e. V )
ofpreima.4 
|- ( ph -> R Fn ( B X. C ) )
Assertion ofpreima 
|- ( ph -> ( `' ( F oF R G ) " D ) = U_ p e. ( `' R " D ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )

Proof

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 syl5rbb 
 |-  ( 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 ) } ) ) )