Metamath Proof Explorer

Theorem fresaunres1

Description: From the union of two functions that agree on the domain overlap, either component can be recovered by restriction. (Contributed by Mario Carneiro, 16-Feb-2015)

Ref Expression
Assertion fresaunres1 ⊢F:A⟶C∧G:B⟶C∧F↾A∩B=G↾A∩B→F∪G↾A=F

Proof

Step Hyp Ref Expression
1 uncom ⊢F∪G=G∪F
2 1 reseq1i ⊢F∪G↾A=G∪F↾A
3 incom ⊢A∩B=B∩A
4 3 reseq2i ⊢F↾A∩B=F↾B∩A
5 3 reseq2i ⊢G↾A∩B=G↾B∩A
6 4 5 eqeq12i ⊢F↾A∩B=G↾A∩B↔F↾B∩A=G↾B∩A
7 eqcom ⊢F↾B∩A=G↾B∩A↔G↾B∩A=F↾B∩A
8 6 7 bitri ⊢F↾A∩B=G↾A∩B↔G↾B∩A=F↾B∩A
9 fresaunres2 ⊢G:B⟶C∧F:A⟶C∧G↾B∩A=F↾B∩A→G∪F↾A=F
10 9 3com12 ⊢F:A⟶C∧G:B⟶C∧G↾B∩A=F↾B∩A→G∪F↾A=F
11 8 10 syl3an3b ⊢F:A⟶C∧G:B⟶C∧F↾A∩B=G↾A∩B→G∪F↾A=F
12 2 11 eqtrid ⊢F:A⟶C∧G:B⟶C∧F↾A∩B=G↾A∩B→F∪G↾A=F