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 ∩ B = G ↾ A ∩ B → F ∪ 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 ∩ B = G ↾ A ∩ B → F ↾ A ∩ B = G ↾ A ∩ B
4 resasplit ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ∪ G = F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A
5 1 2 3 4 syl3an ⊢ F : A ⟶ C ∧ G : B ⟶ C ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ∪ G = F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A
6 5 reseq1d ⊢ F : A ⟶ C ∧ G : B ⟶ C ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ∪ G ↾ B = F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A ↾ B
7 resundir ⊢ F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A ↾ B = F ↾ A ∩ B ↾ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A ↾ B
8 inss2 ⊢ A ∩ B ⊆ B
9 resabs2 ⊢ A ∩ B ⊆ B → F ↾ A ∩ B ↾ B = F ↾ A ∩ B
10 8 9 ax-mp ⊢ F ↾ A ∩ B ↾ B = F ↾ A ∩ B
11 resundir ⊢ F ↾ A ∖ B ∪ G ↾ B ∖ A ↾ B = F ↾ A ∖ B ↾ B ∪ G ↾ B ∖ A ↾ B
12 10 11 uneq12i ⊢ F ↾ A ∩ B ↾ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A ↾ B = F ↾ A ∩ B ∪ F ↾ A ∖ B ↾ B ∪ G ↾ B ∖ A ↾ B
13 dmres ⊢ dom ⁡ F ↾ A ∖ B ↾ B = B ∩ dom ⁡ F ↾ A ∖ B
14 dmres ⊢ dom ⁡ F ↾ A ∖ B = A ∖ B ∩ dom ⁡ F
15 14 ineq2i ⊢ B ∩ dom ⁡ F ↾ A ∖ B = B ∩ A ∖ B ∩ dom ⁡ F
16 disjdif ⊢ B ∩ A ∖ B = ∅
17 16 ineq1i ⊢ B ∩ A ∖ B ∩ dom ⁡ F = ∅ ∩ dom ⁡ F
18 inass ⊢ B ∩ A ∖ B ∩ dom ⁡ F = B ∩ A ∖ B ∩ dom ⁡ F
19 0in ⊢ ∅ ∩ dom ⁡ F = ∅
20 17 18 19 3eqtr3i ⊢ B ∩ A ∖ B ∩ dom ⁡ F = ∅
21 15 20 eqtri ⊢ B ∩ 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 ⊆ B
28 resabs2 ⊢ B ∖ A ⊆ 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 ∪ G ↾ B ∖ A ↾ B = ∅ ∪ G ↾ B ∖ A
31 30 uneq2i ⊢ F ↾ A ∩ B ∪ F ↾ A ∖ B ↾ B ∪ G ↾ B ∖ A ↾ B = F ↾ A ∩ B ∪ ∅ ∪ G ↾ B ∖ A
32 simp3 ⊢ F : A ⟶ C ∧ G : B ⟶ C ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∩ B = G ↾ A ∩ B
33 32 uneq1d ⊢ F : A ⟶ C ∧ G : B ⟶ C ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∩ B ∪ ∅ ∪ G ↾ B ∖ A = G ↾ A ∩ B ∪ ∅ ∪ G ↾ B ∖ A
34 uncom ⊢ ∅ ∪ G ↾ B ∖ A = G ↾ B ∖ A ∪ ∅
35 un0 ⊢ G ↾ B ∖ A ∪ ∅ = G ↾ B ∖ A
36 34 35 eqtri ⊢ ∅ ∪ G ↾ B ∖ A = G ↾ B ∖ A
37 36 uneq2i ⊢ G ↾ A ∩ B ∪ ∅ ∪ G ↾ B ∖ A = G ↾ A ∩ B ∪ G ↾ B ∖ A
38 resundi ⊢ G ↾ A ∩ B ∪ B ∖ A = G ↾ A ∩ B ∪ G ↾ B ∖ A
39 incom ⊢ A ∩ B = B ∩ A
40 39 uneq1i ⊢ A ∩ B ∪ B ∖ A = B ∩ A ∪ B ∖ A
41 inundif ⊢ B ∩ A ∪ B ∖ A = B
42 40 41 eqtri ⊢ A ∩ B ∪ B ∖ A = B
43 42 reseq2i ⊢ G ↾ A ∩ B ∪ 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 eqtrid ⊢ F : A ⟶ C ∧ G : B ⟶ C → G ↾ A ∩ B ∪ B ∖ A = G
48 38 47 eqtr3id ⊢ F : A ⟶ C ∧ G : B ⟶ C → G ↾ A ∩ B ∪ G ↾ B ∖ A = G
49 37 48 eqtrid ⊢ F : A ⟶ C ∧ G : B ⟶ C → G ↾ A ∩ B ∪ ∅ ∪ G ↾ B ∖ A = G
50 49 3adant3 ⊢ F : A ⟶ C ∧ G : B ⟶ C ∧ F ↾ A ∩ B = G ↾ A ∩ B → G ↾ A ∩ B ∪ ∅ ∪ G ↾ B ∖ A = G
51 33 50 eqtrd ⊢ F : A ⟶ C ∧ G : B ⟶ C ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∩ B ∪ ∅ ∪ G ↾ B ∖ A = G
52 31 51 eqtrid ⊢ F : A ⟶ C ∧ G : B ⟶ C ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∩ B ∪ F ↾ A ∖ B ↾ B ∪ G ↾ B ∖ A ↾ B = G
53 12 52 eqtrid ⊢ F : A ⟶ C ∧ G : B ⟶ C ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∩ B ↾ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A ↾ B = G
54 7 53 eqtrid ⊢ F : A ⟶ C ∧ G : B ⟶ C ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A ↾ B = G
55 6 54 eqtrd ⊢ F : A ⟶ C ∧ G : B ⟶ C ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ∪ G ↾ B = G