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	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐴 ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		uncom	⊢ ( 𝐹 ∪ 𝐺 ) = ( 𝐺 ∪ 𝐹 )
2	1	reseq1i	⊢ ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐴 ) = ( ( 𝐺 ∪ 𝐹 ) ↾ 𝐴 )
3		incom	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
4	3	reseq2i	⊢ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐹 ↾ ( 𝐵 ∩ 𝐴 ) )
5	3	reseq2i	⊢ ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐵 ∩ 𝐴 ) )
6	4 5	eqeq12i	⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ↔ ( 𝐹 ↾ ( 𝐵 ∩ 𝐴 ) ) = ( 𝐺 ↾ ( 𝐵 ∩ 𝐴 ) ) )
7		eqcom	⊢ ( ( 𝐹 ↾ ( 𝐵 ∩ 𝐴 ) ) = ( 𝐺 ↾ ( 𝐵 ∩ 𝐴 ) ) ↔ ( 𝐺 ↾ ( 𝐵 ∩ 𝐴 ) ) = ( 𝐹 ↾ ( 𝐵 ∩ 𝐴 ) ) )
8	6 7	bitri	⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ↔ ( 𝐺 ↾ ( 𝐵 ∩ 𝐴 ) ) = ( 𝐹 ↾ ( 𝐵 ∩ 𝐴 ) ) )
9		fresaunres2	⊢ ( ( 𝐺 : 𝐵 ⟶ 𝐶 ∧ 𝐹 : 𝐴 ⟶ 𝐶 ∧ ( 𝐺 ↾ ( 𝐵 ∩ 𝐴 ) ) = ( 𝐹 ↾ ( 𝐵 ∩ 𝐴 ) ) ) → ( ( 𝐺 ∪ 𝐹 ) ↾ 𝐴 ) = 𝐹 )
10	9	3com12	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐺 ↾ ( 𝐵 ∩ 𝐴 ) ) = ( 𝐹 ↾ ( 𝐵 ∩ 𝐴 ) ) ) → ( ( 𝐺 ∪ 𝐹 ) ↾ 𝐴 ) = 𝐹 )
11	8 10	syl3an3b	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐺 ∪ 𝐹 ) ↾ 𝐴 ) = 𝐹 )
12	2 11	syl5eq	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐴 ) = 𝐹 )