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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → 𝐹 : 𝐴 ⟶ 𝐶 )
2 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
3 fssres ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∩ 𝐵 ) ⟶ 𝐶 )
4 1 2 3 sylancl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∩ 𝐵 ) ⟶ 𝐶 )
5 difss ⊢ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴
6 fssres ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) ⟶ 𝐶 )
7 1 5 6 sylancl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) ⟶ 𝐶 )
8 simp2 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → 𝐺 : 𝐵 ⟶ 𝐶 )
9 difss ⊢ ( 𝐵 ∖ 𝐴 ) ⊆ 𝐵
10 fssres ⊢ ( ( 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐵 ∖ 𝐴 ) ⊆ 𝐵 ) → ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) : ( 𝐵 ∖ 𝐴 ) ⟶ 𝐶 )
11 8 9 10 sylancl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) : ( 𝐵 ∖ 𝐴 ) ⟶ 𝐶 )
12 indifdir ⊢ ( ( 𝐴 ∖ 𝐵 ) ∩ ( 𝐵 ∖ 𝐴 ) ) = ( ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) ∖ ( 𝐵 ∩ ( 𝐵 ∖ 𝐴 ) ) )
13 disjdif ⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅
14 13 difeq1i ⊢ ( ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) ∖ ( 𝐵 ∩ ( 𝐵 ∖ 𝐴 ) ) ) = ( ∅ ∖ ( 𝐵 ∩ ( 𝐵 ∖ 𝐴 ) ) )
15 0dif ⊢ ( ∅ ∖ ( 𝐵 ∩ ( 𝐵 ∖ 𝐴 ) ) ) = ∅
16 12 14 15 3eqtri ⊢ ( ( 𝐴 ∖ 𝐵 ) ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅
17 16 a1i ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐴 ∖ 𝐵 ) ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅ )
18 7 11 17 fun2d ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) : ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) ⟶ 𝐶 )
19 indi ⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐴 ∖ 𝐵 ) ) ∪ ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐵 ∖ 𝐴 ) ) )
20 inass ⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐴 ∩ ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) )
21 disjdif ⊢ ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅
22 21 ineq2i ⊢ ( 𝐴 ∩ ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) ) = ( 𝐴 ∩ ∅ )
23 in0 ⊢ ( 𝐴 ∩ ∅ ) = ∅
24 20 22 23 3eqtri ⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅
25 incom ⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
26 25 ineq1i ⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐵 ∖ 𝐴 ) ) = ( ( 𝐵 ∩ 𝐴 ) ∩ ( 𝐵 ∖ 𝐴 ) )
27 inass ⊢ ( ( 𝐵 ∩ 𝐴 ) ∩ ( 𝐵 ∖ 𝐴 ) ) = ( 𝐵 ∩ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) )
28 13 ineq2i ⊢ ( 𝐵 ∩ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) ) = ( 𝐵 ∩ ∅ )
29 in0 ⊢ ( 𝐵 ∩ ∅ ) = ∅
30 27 28 29 3eqtri ⊢ ( ( 𝐵 ∩ 𝐴 ) ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅
31 26 30 eqtri ⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅
32 24 31 uneq12i ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐴 ∖ 𝐵 ) ) ∪ ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐵 ∖ 𝐴 ) ) ) = ( ∅ ∪ ∅ )
33 un0 ⊢ ( ∅ ∪ ∅ ) = ∅
34 19 32 33 3eqtri ⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ∅
35 34 a1i ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐴 ∩ 𝐵 ) ∩ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ∅ )
36 4 18 35 fun2d ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) : ( ( 𝐴 ∩ 𝐵 ) ∪ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) ) ⟶ 𝐶 )
37 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐶 → 𝐹 Fn 𝐴 )
38 ffn ⊢ ( 𝐺 : 𝐵 ⟶ 𝐶 → 𝐺 Fn 𝐵 )
39 id ⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) )
40 resasplit ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐹 ∪ 𝐺 ) = ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) )
41 37 38 39 40 syl3an ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐹 ∪ 𝐺 ) = ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) )
42 41 feq1d ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 ↔ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 ) )
43 un12 ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) )
44 25 uneq1i ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) = ( ( 𝐵 ∩ 𝐴 ) ∪ ( 𝐵 ∖ 𝐴 ) )
45 inundif ⊢ ( ( 𝐵 ∩ 𝐴 ) ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵
46 44 45 eqtri ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵
47 46 uneq2i ⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 )
48 undif1 ⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 )
49 43 47 48 3eqtri ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( 𝐴 ∪ 𝐵 )
50 49 feq2i ⊢ ( ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) : ( ( 𝐴 ∩ 𝐵 ) ∪ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) ) ⟶ 𝐶 ↔ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 )
51 42 50 syl6rbbr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) : ( ( 𝐴 ∩ 𝐵 ) ∪ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) ) ⟶ 𝐶 ↔ ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 ) )
52 36 51 mpbid ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 )