This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 )