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 ⊢FFnA∧GFnB∧F↾A∩B=G↾A∩B→F∪G=F↾A∩B∪F↾A∖B∪G↾B∖A

Proof

Step Hyp Ref Expression
1 fnresdm ⊢FFnA→F↾A=F
2 fnresdm ⊢GFnB→G↾B=G
3 uneq12 ⊢F↾A=F∧G↾B=G→F↾A∪G↾B=F∪G
4 1 2 3 syl2an ⊢FFnA∧GFnB→F↾A∪G↾B=F∪G
5 4 3adant3 ⊢FFnA∧GFnB∧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 ⊢FFnA∧GFnB∧F↾A∩B=G↾A∩B→F↾A∩B=G↾A∩B
19 18 uneq1d ⊢FFnA∧GFnB∧F↾A∩B=G↾A∩B→F↾A∩B∪G↾B∖A=G↾A∩B∪G↾B∖A
20 19 uneq2d ⊢FFnA∧GFnB∧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 ⊢FFnA∧GFnB∧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 ⊢FFnA∧GFnB∧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 ⊢FFnA∧GFnB∧F↾A∩B=G↾A∩B→F↾A∪G↾B=F↾A∩B∪F↾A∖B∪G↾B∖A
27 5 26 eqtr3d ⊢FFnA∧GFnB∧F↾A∩B=G↾A∩B→F∪G=F↾A∩B∪F↾A∖B∪G↾B∖A