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