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