Metamath Proof Explorer

Theorem fresaun

Description: The union of two functions which agree on their common domain is a function. (Contributed by Stefan O'Rear, 9-Oct-2014)

Ref Expression
Assertion fresaun 
|- ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( F u. G ) : ( A u. B ) --> C )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> F : A --> C )
2 inss1 
 |-  ( A i^i B ) C_ A
3 fssres 
 |-  ( ( F : A --> C /\ ( A i^i B ) C_ A ) -> ( F |` ( A i^i B ) ) : ( A i^i B ) --> C )
4 1 2 3 sylancl 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( F |` ( A i^i B ) ) : ( A i^i B ) --> C )
5 difss 
 |-  ( A \ B ) C_ A
6 fssres 
 |-  ( ( F : A --> C /\ ( A \ B ) C_ A ) -> ( F |` ( A \ B ) ) : ( A \ B ) --> C )
7 1 5 6 sylancl 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( F |` ( A \ B ) ) : ( A \ B ) --> C )
8 simp2 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> G : B --> C )
9 difss 
 |-  ( B \ A ) C_ B
10 fssres 
 |-  ( ( G : B --> C /\ ( B \ A ) C_ B ) -> ( G |` ( B \ A ) ) : ( B \ A ) --> C )
11 8 9 10 sylancl 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( G |` ( B \ A ) ) : ( B \ A ) --> C )
12 indifdir 
 |-  ( ( A \ B ) i^i ( B \ A ) ) = ( ( A i^i ( B \ A ) ) \ ( B i^i ( B \ A ) ) )
13 disjdif 
 |-  ( A i^i ( B \ A ) ) = (/)
14 13 difeq1i 
 |-  ( ( A i^i ( B \ A ) ) \ ( B i^i ( B \ A ) ) ) = ( (/) \ ( B i^i ( B \ A ) ) )
15 0dif 
 |-  ( (/) \ ( B i^i ( B \ A ) ) ) = (/)
16 12 14 15 3eqtri 
 |-  ( ( A \ B ) i^i ( B \ A ) ) = (/)
17 16 a1i 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( A \ B ) i^i ( B \ A ) ) = (/) )
18 7 11 17 fun2d 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) : ( ( A \ B ) u. ( B \ A ) ) --> C )
19 indi 
 |-  ( ( A i^i B ) i^i ( ( A \ B ) u. ( B \ A ) ) ) = ( ( ( A i^i B ) i^i ( A \ B ) ) u. ( ( A i^i B ) i^i ( B \ A ) ) )
20 inass 
 |-  ( ( A i^i B ) i^i ( A \ B ) ) = ( A i^i ( B i^i ( A \ B ) ) )
21 disjdif 
 |-  ( B i^i ( A \ B ) ) = (/)
22 21 ineq2i 
 |-  ( A i^i ( B i^i ( A \ B ) ) ) = ( A i^i (/) )
23 in0 
 |-  ( A i^i (/) ) = (/)
24 20 22 23 3eqtri 
 |-  ( ( A i^i B ) i^i ( A \ B ) ) = (/)
25 incom 
 |-  ( A i^i B ) = ( B i^i A )
26 25 ineq1i 
 |-  ( ( A i^i B ) i^i ( B \ A ) ) = ( ( B i^i A ) i^i ( B \ A ) )
27 inass 
 |-  ( ( B i^i A ) i^i ( B \ A ) ) = ( B i^i ( A i^i ( B \ A ) ) )
28 13 ineq2i 
 |-  ( B i^i ( A i^i ( B \ A ) ) ) = ( B i^i (/) )
29 in0 
 |-  ( B i^i (/) ) = (/)
30 27 28 29 3eqtri 
 |-  ( ( B i^i A ) i^i ( B \ A ) ) = (/)
31 26 30 eqtri 
 |-  ( ( A i^i B ) i^i ( B \ A ) ) = (/)
32 24 31 uneq12i 
 |-  ( ( ( A i^i B ) i^i ( A \ B ) ) u. ( ( A i^i B ) i^i ( B \ A ) ) ) = ( (/) u. (/) )
33 un0 
 |-  ( (/) u. (/) ) = (/)
34 19 32 33 3eqtri 
 |-  ( ( A i^i B ) i^i ( ( A \ B ) u. ( B \ A ) ) ) = (/)
35 34 a1i 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( A i^i B ) i^i ( ( A \ B ) u. ( B \ A ) ) ) = (/) )
36 4 18 35 fun2d 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F |` ( A i^i B ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) ) : ( ( A i^i B ) u. ( ( A \ B ) u. ( B \ A ) ) ) --> C )
37 un12 
 |-  ( ( A i^i B ) u. ( ( A \ B ) u. ( B \ A ) ) ) = ( ( A \ B ) u. ( ( A i^i B ) u. ( B \ A ) ) )
38 25 uneq1i 
 |-  ( ( A i^i B ) u. ( B \ A ) ) = ( ( B i^i A ) u. ( B \ A ) )
39 inundif 
 |-  ( ( B i^i A ) u. ( B \ A ) ) = B
40 38 39 eqtri 
 |-  ( ( A i^i B ) u. ( B \ A ) ) = B
41 40 uneq2i 
 |-  ( ( A \ B ) u. ( ( A i^i B ) u. ( B \ A ) ) ) = ( ( A \ B ) u. B )
42 undif1 
 |-  ( ( A \ B ) u. B ) = ( A u. B )
43 37 41 42 3eqtri 
 |-  ( ( A i^i B ) u. ( ( A \ B ) u. ( B \ A ) ) ) = ( A u. B )
44 43 feq2i 
 |-  ( ( ( F |` ( A i^i B ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) ) : ( ( A i^i B ) u. ( ( A \ B ) u. ( B \ A ) ) ) --> C <-> ( ( F |` ( A i^i B ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) ) : ( A u. B ) --> C )
45 ffn 
 |-  ( F : A --> C -> F Fn A )
46 ffn 
 |-  ( G : B --> C -> G Fn B )
47 id 
 |-  ( ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) -> ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) )
48 resasplit 
 |-  ( ( F Fn A /\ G Fn B /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( F u. G ) = ( ( F |` ( A i^i B ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) ) )
49 45 46 47 48 syl3an 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( F u. G ) = ( ( F |` ( A i^i B ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) ) )
50 49 feq1d 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F u. G ) : ( A u. B ) --> C <-> ( ( F |` ( A i^i B ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) ) : ( A u. B ) --> C ) )
51 44 50 bitr4id 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( ( F |` ( A i^i B ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) ) : ( ( A i^i B ) u. ( ( A \ B ) u. ( B \ A ) ) ) --> C <-> ( F u. G ) : ( A u. B ) --> C ) )
52 36 51 mpbid 
 |-  ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( F u. G ) : ( A u. B ) --> C )