Metamath Proof Explorer

Theorem resasplit

Description: If two functions agree on their common domain, express their union as a union of three functions with pairwise disjoint domains. (Contributed by Stefan O'Rear, 9-Oct-2014)

Ref Expression
Assertion resasplit ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ∪ G = F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A

Proof

Step Hyp Ref Expression
1 fnresdm ⊢ F Fn A → F ↾ A = F
2 fnresdm ⊢ G Fn B → G ↾ B = G
3 uneq12 ⊢ F ↾ A = F ∧ G ↾ B = G → F ↾ A ∪ G ↾ B = F ∪ G
4 1 2 3 syl2an ⊢ F Fn A ∧ G Fn B → F ↾ A ∪ G ↾ B = F ∪ G
5 4 3adant3 ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∪ G ↾ B = F ∪ G
6 simp3 ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∩ B = G ↾ A ∩ B
7 6 uneq1d ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∩ B ∪ G ↾ B ∖ A = G ↾ A ∩ B ∪ G ↾ B ∖ A
8 7 uneq2d ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ F ↾ A ∩ B ∪ G ↾ B ∖ A = F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ A ∩ B ∪ G ↾ B ∖ A
9 inundif ⊢ A ∩ B ∪ A ∖ B = A
10 9 reseq2i ⊢ F ↾ A ∩ B ∪ A ∖ B = F ↾ A
11 resundi ⊢ F ↾ A ∩ B ∪ A ∖ B = F ↾ A ∩ B ∪ F ↾ A ∖ B
12 10 11 eqtr3i ⊢ F ↾ A = F ↾ A ∩ B ∪ F ↾ A ∖ B
13 incom ⊢ A ∩ B = B ∩ A
14 13 uneq1i ⊢ A ∩ B ∪ B ∖ A = B ∩ A ∪ B ∖ A
15 inundif ⊢ B ∩ A ∪ B ∖ A = B
16 14 15 eqtri ⊢ A ∩ B ∪ B ∖ A = B
17 16 reseq2i ⊢ G ↾ A ∩ B ∪ B ∖ A = G ↾ B
18 resundi ⊢ G ↾ A ∩ B ∪ B ∖ A = G ↾ A ∩ B ∪ G ↾ B ∖ A
19 17 18 eqtr3i ⊢ G ↾ B = G ↾ A ∩ B ∪ G ↾ B ∖ A
20 12 19 uneq12i ⊢ F ↾ A ∪ G ↾ B = F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ A ∩ B ∪ G ↾ B ∖ A
21 8 20 syl6reqr ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∪ G ↾ B = F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ F ↾ A ∩ B ∪ G ↾ B ∖ A
22 un4 ⊢ F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ F ↾ A ∩ B ∪ G ↾ B ∖ A = F ↾ A ∩ B ∪ F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A
23 21 22 syl6eq ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∪ G ↾ B = F ↾ A ∩ B ∪ F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A
24 unidm ⊢ F ↾ A ∩ B ∪ F ↾ A ∩ B = F ↾ A ∩ B
25 24 uneq1i ⊢ F ↾ A ∩ B ∪ F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A = F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A
26 23 25 syl6eq ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∪ G ↾ B = F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A
27 5 26 eqtr3d ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ∪ G = F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A