Theorem fnund

Description: The union of two functions with disjoint domains, a deduction version. (Contributed by metakunt, 28-May-2024)

	Ref	Expression
Hypotheses	fnund.1	$$⊢\phi \to FFnA$$
	fnund.2	$$⊢\phi \to GFnB$$
	fnund.3	$$⊢\phi \to A\cap B=\varnothing$$
Assertion	fnund	$$⊢\phi \to \left(F\cup G\right)Fn\left(A\cup B\right)$$

Proof

Step	Hyp	Ref	Expression
1		fnund.1	$$⊢\phi \to FFnA$$
2		fnund.2	$$⊢\phi \to GFnB$$
3		fnund.3	$$⊢\phi \to A\cap B=\varnothing$$
4		fnun	$$⊢\left(\left(FFnA\wedge GFnB\right)\wedge A\cap B=\varnothing \right)\to \left(F\cup G\right)Fn\left(A\cup B\right)$$
5	1 2 3 4	syl21anc	$$⊢\phi \to \left(F\cup G\right)Fn\left(A\cup B\right)$$