Metamath Proof Explorer

Theorem fresaunres2

Description: From the union of two functions that agree on the domain overlap, either component can be recovered by restriction. (Contributed by Stefan O'Rear, 9-Oct-2014)

Ref Expression
Assertion fresaunres2 
|- ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F u. G ) |` B ) = G )

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( F : A --> C -> F Fn A )
2 ffn 
 |-  ( G : B --> C -> G Fn B )
3 id 
 |-  ( ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) -> ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) )
4 resasplit 
 |-  ( ( F Fn A /\ G Fn B /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( F u. G ) = ( ( F |` ( A i^i B ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) ) )
5 1 2 3 4 syl3an 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( F u. G ) = ( ( F |` ( A i^i B ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) ) )
6 5 reseq1d 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F u. G ) |` B ) = ( ( ( F |` ( A i^i B ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) ) |` B ) )
7 resundir 
 |-  ( ( ( F |` ( A i^i B ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) ) |` B ) = ( ( ( F |` ( A i^i B ) ) |` B ) u. ( ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) |` B ) )
8 inss2 
 |-  ( A i^i B ) C_ B
9 resabs2 
 |-  ( ( A i^i B ) C_ B -> ( ( F |` ( A i^i B ) ) |` B ) = ( F |` ( A i^i B ) ) )
10 8 9 ax-mp 
 |-  ( ( F |` ( A i^i B ) ) |` B ) = ( F |` ( A i^i B ) )
11 resundir 
 |-  ( ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) |` B ) = ( ( ( F |` ( A \ B ) ) |` B ) u. ( ( G |` ( B \ A ) ) |` B ) )
12 10 11 uneq12i 
 |-  ( ( ( F |` ( A i^i B ) ) |` B ) u. ( ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) |` B ) ) = ( ( F |` ( A i^i B ) ) u. ( ( ( F |` ( A \ B ) ) |` B ) u. ( ( G |` ( B \ A ) ) |` B ) ) )
13 dmres 
 |-  dom ( ( F |` ( A \ B ) ) |` B ) = ( B i^i dom ( F |` ( A \ B ) ) )
14 dmres 
 |-  dom ( F |` ( A \ B ) ) = ( ( A \ B ) i^i dom F )
15 14 ineq2i 
 |-  ( B i^i dom ( F |` ( A \ B ) ) ) = ( B i^i ( ( A \ B ) i^i dom F ) )
16 disjdif 
 |-  ( B i^i ( A \ B ) ) = (/)
17 16 ineq1i 
 |-  ( ( B i^i ( A \ B ) ) i^i dom F ) = ( (/) i^i dom F )
18 inass 
 |-  ( ( B i^i ( A \ B ) ) i^i dom F ) = ( B i^i ( ( A \ B ) i^i dom F ) )
19 0in 
 |-  ( (/) i^i dom F ) = (/)
20 17 18 19 3eqtr3i 
 |-  ( B i^i ( ( A \ B ) i^i dom F ) ) = (/)
21 15 20 eqtri 
 |-  ( B i^i dom ( F |` ( A \ B ) ) ) = (/)
22 13 21 eqtri 
 |-  dom ( ( F |` ( A \ B ) ) |` B ) = (/)
23 relres 
 |-  Rel ( ( F |` ( A \ B ) ) |` B )
24 reldm0 
 |-  ( Rel ( ( F |` ( A \ B ) ) |` B ) -> ( ( ( F |` ( A \ B ) ) |` B ) = (/) <-> dom ( ( F |` ( A \ B ) ) |` B ) = (/) ) )
25 23 24 ax-mp 
 |-  ( ( ( F |` ( A \ B ) ) |` B ) = (/) <-> dom ( ( F |` ( A \ B ) ) |` B ) = (/) )
26 22 25 mpbir 
 |-  ( ( F |` ( A \ B ) ) |` B ) = (/)
27 difss 
 |-  ( B \ A ) C_ B
28 resabs2 
 |-  ( ( B \ A ) C_ B -> ( ( G |` ( B \ A ) ) |` B ) = ( G |` ( B \ A ) ) )
29 27 28 ax-mp 
 |-  ( ( G |` ( B \ A ) ) |` B ) = ( G |` ( B \ A ) )
30 26 29 uneq12i 
 |-  ( ( ( F |` ( A \ B ) ) |` B ) u. ( ( G |` ( B \ A ) ) |` B ) ) = ( (/) u. ( G |` ( B \ A ) ) )
31 30 uneq2i 
 |-  ( ( F |` ( A i^i B ) ) u. ( ( ( F |` ( A \ B ) ) |` B ) u. ( ( G |` ( B \ A ) ) |` B ) ) ) = ( ( F |` ( A i^i B ) ) u. ( (/) u. ( G |` ( B \ A ) ) ) )
32 simp3 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) )
33 32 uneq1d 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F |` ( A i^i B ) ) u. ( (/) u. ( G |` ( B \ A ) ) ) ) = ( ( G |` ( A i^i B ) ) u. ( (/) u. ( G |` ( B \ A ) ) ) ) )
34 uncom 
 |-  ( (/) u. ( G |` ( B \ A ) ) ) = ( ( G |` ( B \ A ) ) u. (/) )
35 un0 
 |-  ( ( G |` ( B \ A ) ) u. (/) ) = ( G |` ( B \ A ) )
36 34 35 eqtri 
 |-  ( (/) u. ( G |` ( B \ A ) ) ) = ( G |` ( B \ A ) )
37 36 uneq2i 
 |-  ( ( G |` ( A i^i B ) ) u. ( (/) u. ( G |` ( B \ A ) ) ) ) = ( ( G |` ( A i^i B ) ) u. ( G |` ( B \ A ) ) )
38 resundi 
 |-  ( G |` ( ( A i^i B ) u. ( B \ A ) ) ) = ( ( G |` ( A i^i B ) ) u. ( G |` ( B \ A ) ) )
39 incom 
 |-  ( A i^i B ) = ( B i^i A )
40 39 uneq1i 
 |-  ( ( A i^i B ) u. ( B \ A ) ) = ( ( B i^i A ) u. ( B \ A ) )
41 inundif 
 |-  ( ( B i^i A ) u. ( B \ A ) ) = B
42 40 41 eqtri 
 |-  ( ( A i^i B ) u. ( B \ A ) ) = B
43 42 reseq2i 
 |-  ( G |` ( ( A i^i B ) u. ( B \ A ) ) ) = ( G |` B )
44 fnresdm 
 |-  ( G Fn B -> ( G |` B ) = G )
45 2 44 syl 
 |-  ( G : B --> C -> ( G |` B ) = G )
46 45 adantl 
 |-  ( ( F : A --> C /\ G : B --> C ) -> ( G |` B ) = G )
47 43 46 syl5eq 
 |-  ( ( F : A --> C /\ G : B --> C ) -> ( G |` ( ( A i^i B ) u. ( B \ A ) ) ) = G )
48 38 47 eqtr3id 
 |-  ( ( F : A --> C /\ G : B --> C ) -> ( ( G |` ( A i^i B ) ) u. ( G |` ( B \ A ) ) ) = G )
49 37 48 syl5eq 
 |-  ( ( F : A --> C /\ G : B --> C ) -> ( ( G |` ( A i^i B ) ) u. ( (/) u. ( G |` ( B \ A ) ) ) ) = G )
50 49 3adant3 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( G |` ( A i^i B ) ) u. ( (/) u. ( G |` ( B \ A ) ) ) ) = G )
51 33 50 eqtrd 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F |` ( A i^i B ) ) u. ( (/) u. ( G |` ( B \ A ) ) ) ) = G )
52 31 51 syl5eq 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F |` ( A i^i B ) ) u. ( ( ( F |` ( A \ B ) ) |` B ) u. ( ( G |` ( B \ A ) ) |` B ) ) ) = G )
53 12 52 syl5eq 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( ( F |` ( A i^i B ) ) |` B ) u. ( ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) |` B ) ) = G )
54 7 53 syl5eq 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( ( F |` ( A i^i B ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) ) |` B ) = G )
55 6 54 eqtrd 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F u. G ) |` B ) = G )