Theorem foun

Description: The union of two onto functions with disjoint domains is an onto function. (Contributed by Mario Carneiro, 22-Jun-2016)

	Ref	Expression
Assertion	foun	⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –onto→ ( 𝐵 ∪ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		fofn	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 Fn 𝐴 )
2		fofn	⊢ ( 𝐺 : 𝐶 –onto→ 𝐷 → 𝐺 Fn 𝐶 )
3	1 2	anim12i	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) → ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶 ) )
4		fnun	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶 ) ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐶 ) )
5	3 4	sylan	⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐶 ) )
6		rnun	⊢ ran ( 𝐹 ∪ 𝐺 ) = ( ran 𝐹 ∪ ran 𝐺 )
7		forn	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
8	7	ad2antrr	⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ran 𝐹 = 𝐵 )
9		forn	⊢ ( 𝐺 : 𝐶 –onto→ 𝐷 → ran 𝐺 = 𝐷 )
10	9	ad2antlr	⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ran 𝐺 = 𝐷 )
11	8 10	uneq12d	⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ( ran 𝐹 ∪ ran 𝐺 ) = ( 𝐵 ∪ 𝐷 ) )
12	6 11	syl5eq	⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ran ( 𝐹 ∪ 𝐺 ) = ( 𝐵 ∪ 𝐷 ) )
13		df-fo	⊢ ( ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –onto→ ( 𝐵 ∪ 𝐷 ) ↔ ( ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐶 ) ∧ ran ( 𝐹 ∪ 𝐺 ) = ( 𝐵 ∪ 𝐷 ) ) )
14	5 12 13	sylanbrc	⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –onto→ ( 𝐵 ∪ 𝐷 ) )