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	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	fnund.2	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
	fnund.3	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
Assertion	fnund	⊢ ( 𝜑 → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fnund.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		fnund.2	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
3		fnund.3	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
4		fnun	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐵 ) )
5	1 2 3 4	syl21anc	⊢ ( 𝜑 → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐵 ) )