Theorem fun2d

Description: The union of functions with disjoint domains is a function, deduction version of fun2 . (Contributed by AV, 11-Oct-2020) (Revised by AV, 24-Oct-2021)

	Ref	Expression
Hypotheses	fun2d.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )
	fun2d.g	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐶 )
	fun2d.i	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
Assertion	fun2d	⊢ ( 𝜑 → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fun2d.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )
2		fun2d.g	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐶 )
3		fun2d.i	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
4		fun2	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 )
5	1 2 3 4	syl21anc	⊢ ( 𝜑 → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 )