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	$⊢ ((F : A \underset{onto}{⟶} B \land G : C \underset{onto}{⟶} D) \land A \cap C = \emptyset) \to (F \cup G) : A \cup C \underset{onto}{⟶} B \cup D$

Step	Hyp	Ref	Expression
1		fofn	$⊢ F : A \underset{onto}{⟶} B \to F Fn A$
2		fofn	$⊢ G : C \underset{onto}{⟶} D \to G Fn C$
3	1 2	anim12i	$⊢ (F : A \underset{onto}{⟶} B \land G : C \underset{onto}{⟶} D) \to (F Fn A \land G Fn C)$
4		fnun	$⊢ ((F Fn A \land G Fn C) \land A \cap C = \emptyset) \to (F \cup G) Fn (A \cup C)$
5	3 4	sylan	$⊢ ((F : A \underset{onto}{⟶} B \land G : C \underset{onto}{⟶} D) \land A \cap C = \emptyset) \to (F \cup G) Fn (A \cup C)$
6		rnun	$⊢ ran (F \cup G) = ran F \cup ran G$
7		forn	$⊢ F : A \underset{onto}{⟶} B \to ran F = B$
8	7	ad2antrr	$⊢ ((F : A \underset{onto}{⟶} B \land G : C \underset{onto}{⟶} D) \land A \cap C = \emptyset) \to ran F = B$
9		forn	$⊢ G : C \underset{onto}{⟶} D \to ran G = D$
10	9	ad2antlr	$⊢ ((F : A \underset{onto}{⟶} B \land G : C \underset{onto}{⟶} D) \land A \cap C = \emptyset) \to ran G = D$
11	8 10	uneq12d	$⊢ ((F : A \underset{onto}{⟶} B \land G : C \underset{onto}{⟶} D) \land A \cap C = \emptyset) \to ran F \cup ran G = B \cup D$
12	6 11	eqtrid	$⊢ ((F : A \underset{onto}{⟶} B \land G : C \underset{onto}{⟶} D) \land A \cap C = \emptyset) \to ran (F \cup G) = B \cup D$
13		df-fo	$⊢ (F \cup G) : A \cup C \underset{onto}{⟶} B \cup D \leftrightarrow ((F \cup G) Fn (A \cup C) \land ran (F \cup G) = B \cup D)$
14	5 12 13	sylanbrc	$⊢ ((F : A \underset{onto}{⟶} B \land G : C \underset{onto}{⟶} D) \land A \cap C = \emptyset) \to (F \cup G) : A \cup C \underset{onto}{⟶} B \cup D$

Metamath Proof Explorer