Theorem fun2

Description: The union of two functions with disjoint domains. (Contributed by Mario Carneiro, 12-Mar-2015)

	Ref	Expression
Assertion	fun2	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fun	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ ( 𝐶 ∪ 𝐶 ) )
2		unidm	⊢ ( 𝐶 ∪ 𝐶 ) = 𝐶
3		feq3	⊢ ( ( 𝐶 ∪ 𝐶 ) = 𝐶 → ( ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ ( 𝐶 ∪ 𝐶 ) ↔ ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 ) )
4	2 3	ax-mp	⊢ ( ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ ( 𝐶 ∪ 𝐶 ) ↔ ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 )
5	1 4	sylib	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 )