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 i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F u. G ) |` A ) = F )

Proof

Step	Hyp	Ref	Expression
1		uncom	|- ( F u. G ) = ( G u. F )
2	1	reseq1i	|- ( ( F u. G ) |` A ) = ( ( G u. F ) |` A )
3		incom	|- ( A i^i B ) = ( B i^i A )
4	3	reseq2i	|- ( F |` ( A i^i B ) ) = ( F |` ( B i^i A ) )
5	3	reseq2i	|- ( G |` ( A i^i B ) ) = ( G |` ( B i^i A ) )
6	4 5	eqeq12i	|- ( ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) <-> ( F |` ( B i^i A ) ) = ( G |` ( B i^i A ) ) )
7		eqcom	|- ( ( F |` ( B i^i A ) ) = ( G |` ( B i^i A ) ) <-> ( G |` ( B i^i A ) ) = ( F |` ( B i^i A ) ) )
8	6 7	bitri	|- ( ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) <-> ( G |` ( B i^i A ) ) = ( F |` ( B i^i A ) ) )
9		fresaunres2	|- ( ( G : B --> C /\ F : A --> C /\ ( G |` ( B i^i A ) ) = ( F |` ( B i^i A ) ) ) -> ( ( G u. F ) |` A ) = F )
10	9	3com12	|- ( ( F : A --> C /\ G : B --> C /\ ( G |` ( B i^i A ) ) = ( F |` ( B i^i A ) ) ) -> ( ( G u. F ) |` A ) = F )
11	8 10	syl3an3b	|- ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( G u. F ) |` A ) = F )
12	2 11	eqtrid	|- ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F u. G ) |` A ) = F )