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