Metamath Proof Explorer

Theorem fnun

Description: The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004)

Ref Expression
Assertion fnun ⊢ F Fn A ∧ G Fn B ∧ A ∩ B = ∅ → F ∪ G Fn A ∪ B

Proof

Step Hyp Ref Expression
1 df-fn ⊢ F Fn A ↔ Fun ⁡ F ∧ dom ⁡ F = A
2 df-fn ⊢ G Fn B ↔ Fun ⁡ G ∧ dom ⁡ G = B
3 ineq12 ⊢ dom ⁡ F = A ∧ dom ⁡ G = B → dom ⁡ F ∩ dom ⁡ G = A ∩ B
4 3 eqeq1d ⊢ dom ⁡ F = A ∧ dom ⁡ G = B → dom ⁡ F ∩ dom ⁡ G = ∅ ↔ A ∩ B = ∅
5 4 anbi2d ⊢ dom ⁡ F = A ∧ dom ⁡ G = B → Fun ⁡ F ∧ Fun ⁡ G ∧ dom ⁡ F ∩ dom ⁡ G = ∅ ↔ Fun ⁡ F ∧ Fun ⁡ G ∧ A ∩ B = ∅
6 funun ⊢ Fun ⁡ F ∧ Fun ⁡ G ∧ dom ⁡ F ∩ dom ⁡ G = ∅ → Fun ⁡ F ∪ G
7 5 6 biimtrrdi ⊢ dom ⁡ F = A ∧ dom ⁡ G = B → Fun ⁡ F ∧ Fun ⁡ G ∧ A ∩ B = ∅ → Fun ⁡ F ∪ G
8 dmun ⊢ dom ⁡ F ∪ G = dom ⁡ F ∪ dom ⁡ G
9 uneq12 ⊢ dom ⁡ F = A ∧ dom ⁡ G = B → dom ⁡ F ∪ dom ⁡ G = A ∪ B
10 8 9 eqtrid ⊢ dom ⁡ F = A ∧ dom ⁡ G = B → dom ⁡ F ∪ G = A ∪ B
11 7 10 jctird ⊢ dom ⁡ F = A ∧ dom ⁡ G = B → Fun ⁡ F ∧ Fun ⁡ G ∧ A ∩ B = ∅ → Fun ⁡ F ∪ G ∧ dom ⁡ F ∪ G = A ∪ B
12 df-fn ⊢ F ∪ G Fn A ∪ B ↔ Fun ⁡ F ∪ G ∧ dom ⁡ F ∪ G = A ∪ B
13 11 12 imbitrrdi ⊢ dom ⁡ F = A ∧ dom ⁡ G = B → Fun ⁡ F ∧ Fun ⁡ G ∧ A ∩ B = ∅ → F ∪ G Fn A ∪ B
14 13 expd ⊢ dom ⁡ F = A ∧ dom ⁡ G = B → Fun ⁡ F ∧ Fun ⁡ G → A ∩ B = ∅ → F ∪ G Fn A ∪ B
15 14 impcom ⊢ Fun ⁡ F ∧ Fun ⁡ G ∧ dom ⁡ F = A ∧ dom ⁡ G = B → A ∩ B = ∅ → F ∪ G Fn A ∪ B
16 15 an4s ⊢ Fun ⁡ F ∧ dom ⁡ F = A ∧ Fun ⁡ G ∧ dom ⁡ G = B → A ∩ B = ∅ → F ∪ G Fn A ∪ B
17 1 2 16 syl2anb ⊢ F Fn A ∧ G Fn B → A ∩ B = ∅ → F ∪ G Fn A ∪ B
18 17 imp ⊢ F Fn A ∧ G Fn B ∧ A ∩ B = ∅ → F ∪ G Fn A ∪ B