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 inundif A B A B = A
7 6 reseq2i F A B A B = F A
8 resundi F A B A B = F A B F A B
9 7 8 eqtr3i F A = F A B F A B
10 incom A B = B A
11 10 uneq1i A B B A = B A B A
12 inundif B A B A = B
13 11 12 eqtri A B B A = B
14 13 reseq2i G A B B A = G B
15 resundi G A B B A = G A B G B A
16 14 15 eqtr3i G B = G A B G B A
17 9 16 uneq12i F A G B = F A B F A B G A B G B A
18 simp3 F Fn A G Fn B F A B = G A B F A B = G A B
19 18 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
20 19 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
21 17 20 eqtr4id 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 eqtrdi 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 eqtrdi 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