Metamath Proof Explorer


Theorem ofpreima2

Description: Express the preimage of a function operation as a union of preimages. This version of ofpreima iterates the union over a smaller set. (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 ofpreima2
|- ( ph -> ( `' ( F oF R G ) " D ) = U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' 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 1 2 3 4 ofpreima
 |-  ( ph -> ( `' ( F oF R G ) " D ) = U_ p e. ( `' R " D ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
6 inundif
 |-  ( ( ( `' R " D ) i^i ( ran F X. ran G ) ) u. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) = ( `' R " D )
7 iuneq1
 |-  ( ( ( ( `' R " D ) i^i ( ran F X. ran G ) ) u. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) = ( `' R " D ) -> U_ p e. ( ( ( `' R " D ) i^i ( ran F X. ran G ) ) u. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = U_ p e. ( `' R " D ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
8 6 7 ax-mp
 |-  U_ p e. ( ( ( `' R " D ) i^i ( ran F X. ran G ) ) u. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = U_ p e. ( `' R " D ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) )
9 iunxun
 |-  U_ p e. ( ( ( `' R " D ) i^i ( ran F X. ran G ) ) u. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = ( U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) u. U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
10 8 9 eqtr3i
 |-  U_ p e. ( `' R " D ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = ( U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) u. U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
11 5 10 eqtrdi
 |-  ( ph -> ( `' ( F oF R G ) " D ) = ( U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) u. U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) )
12 simpr
 |-  ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) )
13 12 eldifbd
 |-  ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> -. p e. ( ran F X. ran G ) )
14 cnvimass
 |-  ( `' R " D ) C_ dom R
15 4 fndmd
 |-  ( ph -> dom R = ( B X. C ) )
16 14 15 sseqtrid
 |-  ( ph -> ( `' R " D ) C_ ( B X. C ) )
17 16 ssdifssd
 |-  ( ph -> ( ( `' R " D ) \ ( ran F X. ran G ) ) C_ ( B X. C ) )
18 17 sselda
 |-  ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> p e. ( B X. C ) )
19 1st2nd2
 |-  ( p e. ( B X. C ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
20 elxp6
 |-  ( p e. ( ran F X. ran G ) <-> ( p = <. ( 1st ` p ) , ( 2nd ` p ) >. /\ ( ( 1st ` p ) e. ran F /\ ( 2nd ` p ) e. ran G ) ) )
21 20 simplbi2
 |-  ( p = <. ( 1st ` p ) , ( 2nd ` p ) >. -> ( ( ( 1st ` p ) e. ran F /\ ( 2nd ` p ) e. ran G ) -> p e. ( ran F X. ran G ) ) )
22 18 19 21 3syl
 |-  ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> ( ( ( 1st ` p ) e. ran F /\ ( 2nd ` p ) e. ran G ) -> p e. ( ran F X. ran G ) ) )
23 13 22 mtod
 |-  ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> -. ( ( 1st ` p ) e. ran F /\ ( 2nd ` p ) e. ran G ) )
24 ianor
 |-  ( -. ( ( 1st ` p ) e. ran F /\ ( 2nd ` p ) e. ran G ) <-> ( -. ( 1st ` p ) e. ran F \/ -. ( 2nd ` p ) e. ran G ) )
25 23 24 sylib
 |-  ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> ( -. ( 1st ` p ) e. ran F \/ -. ( 2nd ` p ) e. ran G ) )
26 disjsn
 |-  ( ( ran F i^i { ( 1st ` p ) } ) = (/) <-> -. ( 1st ` p ) e. ran F )
27 disjsn
 |-  ( ( ran G i^i { ( 2nd ` p ) } ) = (/) <-> -. ( 2nd ` p ) e. ran G )
28 26 27 orbi12i
 |-  ( ( ( ran F i^i { ( 1st ` p ) } ) = (/) \/ ( ran G i^i { ( 2nd ` p ) } ) = (/) ) <-> ( -. ( 1st ` p ) e. ran F \/ -. ( 2nd ` p ) e. ran G ) )
29 25 28 sylibr
 |-  ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> ( ( ran F i^i { ( 1st ` p ) } ) = (/) \/ ( ran G i^i { ( 2nd ` p ) } ) = (/) ) )
30 1 ffnd
 |-  ( ph -> F Fn A )
31 dffn3
 |-  ( F Fn A <-> F : A --> ran F )
32 30 31 sylib
 |-  ( ph -> F : A --> ran F )
33 2 ffnd
 |-  ( ph -> G Fn A )
34 dffn3
 |-  ( G Fn A <-> G : A --> ran G )
35 33 34 sylib
 |-  ( ph -> G : A --> ran G )
36 35 adantr
 |-  ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> G : A --> ran G )
37 fimacnvdisj
 |-  ( ( F : A --> ran F /\ ( ran F i^i { ( 1st ` p ) } ) = (/) ) -> ( `' F " { ( 1st ` p ) } ) = (/) )
38 ineq1
 |-  ( ( `' F " { ( 1st ` p ) } ) = (/) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = ( (/) i^i ( `' G " { ( 2nd ` p ) } ) ) )
39 0in
 |-  ( (/) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/)
40 38 39 eqtrdi
 |-  ( ( `' F " { ( 1st ` p ) } ) = (/) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) )
41 37 40 syl
 |-  ( ( F : A --> ran F /\ ( ran F i^i { ( 1st ` p ) } ) = (/) ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) )
42 41 ex
 |-  ( F : A --> ran F -> ( ( ran F i^i { ( 1st ` p ) } ) = (/) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) ) )
43 fimacnvdisj
 |-  ( ( G : A --> ran G /\ ( ran G i^i { ( 2nd ` p ) } ) = (/) ) -> ( `' G " { ( 2nd ` p ) } ) = (/) )
44 ineq2
 |-  ( ( `' G " { ( 2nd ` p ) } ) = (/) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = ( ( `' F " { ( 1st ` p ) } ) i^i (/) ) )
45 in0
 |-  ( ( `' F " { ( 1st ` p ) } ) i^i (/) ) = (/)
46 44 45 eqtrdi
 |-  ( ( `' G " { ( 2nd ` p ) } ) = (/) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) )
47 43 46 syl
 |-  ( ( G : A --> ran G /\ ( ran G i^i { ( 2nd ` p ) } ) = (/) ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) )
48 47 ex
 |-  ( G : A --> ran G -> ( ( ran G i^i { ( 2nd ` p ) } ) = (/) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) ) )
49 42 48 jaao
 |-  ( ( F : A --> ran F /\ G : A --> ran G ) -> ( ( ( ran F i^i { ( 1st ` p ) } ) = (/) \/ ( ran G i^i { ( 2nd ` p ) } ) = (/) ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) ) )
50 32 36 49 syl2an2r
 |-  ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> ( ( ( ran F i^i { ( 1st ` p ) } ) = (/) \/ ( ran G i^i { ( 2nd ` p ) } ) = (/) ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) ) )
51 29 50 mpd
 |-  ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) )
52 51 iuneq2dv
 |-  ( ph -> U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) (/) )
53 iun0
 |-  U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) (/) = (/)
54 52 53 eqtrdi
 |-  ( ph -> U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) )
55 54 uneq2d
 |-  ( ph -> ( U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) u. U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) = ( U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) u. (/) ) )
56 un0
 |-  ( U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) u. (/) ) = U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) )
57 55 56 eqtrdi
 |-  ( ph -> ( U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) u. U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) = U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
58 11 57 eqtrd
 |-  ( ph -> ( `' ( F oF R G ) " D ) = U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )