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 ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐵 ) = 𝐺 )

Proof

Step Hyp Ref Expression
1 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐶 → 𝐹 Fn 𝐴 )
2 ffn ⊢ ( 𝐺 : 𝐵 ⟶ 𝐶 → 𝐺 Fn 𝐵 )
3 id ⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) )
4 resasplit ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐹 ∪ 𝐺 ) = ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) )
5 1 2 3 4 syl3an ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐹 ∪ 𝐺 ) = ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) )
6 5 reseq1d ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐵 ) = ( ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) ↾ 𝐵 ) )
7 resundir ⊢ ( ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) ↾ 𝐵 ) = ( ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ↾ 𝐵 ) ∪ ( ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ↾ 𝐵 ) )
8 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
9 resabs2 ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ↾ 𝐵 ) = ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) )
10 8 9 ax-mp ⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ↾ 𝐵 ) = ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) )
11 resundir ⊢ ( ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ↾ 𝐵 ) = ( ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ↾ 𝐵 ) ∪ ( ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ↾ 𝐵 ) )
12 10 11 uneq12i ⊢ ( ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ↾ 𝐵 ) ∪ ( ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ↾ 𝐵 ) ) = ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ↾ 𝐵 ) ∪ ( ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ↾ 𝐵 ) ) )
13 dmres ⊢ dom ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ↾ 𝐵 ) = ( 𝐵 ∩ dom ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) )
14 dmres ⊢ dom ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝐴 ∖ 𝐵 ) ∩ dom 𝐹 )
15 14 ineq2i ⊢ ( 𝐵 ∩ dom ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ) = ( 𝐵 ∩ ( ( 𝐴 ∖ 𝐵 ) ∩ dom 𝐹 ) )
16 disjdif ⊢ ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅
17 16 ineq1i ⊢ ( ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) ∩ dom 𝐹 ) = ( ∅ ∩ dom 𝐹 )
18 inass ⊢ ( ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) ∩ dom 𝐹 ) = ( 𝐵 ∩ ( ( 𝐴 ∖ 𝐵 ) ∩ dom 𝐹 ) )
19 0in ⊢ ( ∅ ∩ dom 𝐹 ) = ∅
20 17 18 19 3eqtr3i ⊢ ( 𝐵 ∩ ( ( 𝐴 ∖ 𝐵 ) ∩ dom 𝐹 ) ) = ∅
21 15 20 eqtri ⊢ ( 𝐵 ∩ dom ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ) = ∅
22 13 21 eqtri ⊢ dom ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ↾ 𝐵 ) = ∅
23 relres ⊢ Rel ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ↾ 𝐵 )
24 reldm0 ⊢ ( Rel ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ↾ 𝐵 ) → ( ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ↾ 𝐵 ) = ∅ ↔ dom ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ↾ 𝐵 ) = ∅ ) )
25 23 24 ax-mp ⊢ ( ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ↾ 𝐵 ) = ∅ ↔ dom ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ↾ 𝐵 ) = ∅ )
26 22 25 mpbir ⊢ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ↾ 𝐵 ) = ∅
27 difss ⊢ ( 𝐵 ∖ 𝐴 ) ⊆ 𝐵
28 resabs2 ⊢ ( ( 𝐵 ∖ 𝐴 ) ⊆ 𝐵 → ( ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ↾ 𝐵 ) = ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) )
29 27 28 ax-mp ⊢ ( ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ↾ 𝐵 ) = ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) )
30 26 29 uneq12i ⊢ ( ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ↾ 𝐵 ) ∪ ( ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ↾ 𝐵 ) ) = ( ∅ ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) )
31 30 uneq2i ⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ↾ 𝐵 ) ∪ ( ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ↾ 𝐵 ) ) ) = ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ∅ ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) )
32 simp3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) )
33 32 uneq1d ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ∅ ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) = ( ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ∅ ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) )
34 uncom ⊢ ( ∅ ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) = ( ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ∪ ∅ )
35 un0 ⊢ ( ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ∪ ∅ ) = ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) )
36 34 35 eqtri ⊢ ( ∅ ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) = ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) )
37 36 uneq2i ⊢ ( ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ∅ ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) = ( ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) )
38 resundi ⊢ ( 𝐺 ↾ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) )
39 incom ⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
40 39 uneq1i ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) = ( ( 𝐵 ∩ 𝐴 ) ∪ ( 𝐵 ∖ 𝐴 ) )
41 inundif ⊢ ( ( 𝐵 ∩ 𝐴 ) ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵
42 40 41 eqtri ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵
43 42 reseq2i ⊢ ( 𝐺 ↾ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( 𝐺 ↾ 𝐵 )
44 fnresdm ⊢ ( 𝐺 Fn 𝐵 → ( 𝐺 ↾ 𝐵 ) = 𝐺 )
45 2 44 syl ⊢ ( 𝐺 : 𝐵 ⟶ 𝐶 → ( 𝐺 ↾ 𝐵 ) = 𝐺 )
46 45 adantl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ) → ( 𝐺 ↾ 𝐵 ) = 𝐺 )
47 43 46 syl5eq ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ) → ( 𝐺 ↾ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) ) = 𝐺 )
48 38 47 eqtr3id ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ) → ( ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) = 𝐺 )
49 37 48 syl5eq ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ) → ( ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ∅ ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) = 𝐺 )
50 49 3adant3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ∅ ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) = 𝐺 )
51 33 50 eqtrd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ∅ ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) = 𝐺 )
52 31 51 syl5eq ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ↾ 𝐵 ) ∪ ( ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ↾ 𝐵 ) ) ) = 𝐺 )
53 12 52 syl5eq ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ↾ 𝐵 ) ∪ ( ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ↾ 𝐵 ) ) = 𝐺 )
54 7 53 syl5eq ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) ↾ 𝐵 ) = 𝐺 )
55 6 54 eqtrd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐵 ) = 𝐺 )