fununfun

Description: If the union of classes is a function, the classes itselves are functions. (Contributed by AV, 18-Jul-2019)

		Ref	Expression
	Assertion	fununfun	$⊢ Fun (F \cup G) \to (Fun F \land Fun G)$

Step	Hyp	Ref	Expression
1		funrel	$⊢ Fun (F \cup G) \to Rel (F \cup G)$
2		relun	$⊢ Rel (F \cup G) \leftrightarrow (Rel F \land Rel G)$
3	1 2	sylib	$⊢ Fun (F \cup G) \to (Rel F \land Rel G)$
4		simpl	$⊢ (Rel F \land Rel G) \to Rel F$
5		fununmo	$⊢ Fun (F \cup G) \to \exists^{*} y x F y$
6	5	alrimiv	$⊢ Fun (F \cup G) \to \forall x \exists^{*} y x F y$
7	4 6	anim12i	$⊢ ((Rel F \land Rel G) \land Fun (F \cup G)) \to (Rel F \land \forall x \exists^{*} y x F y)$
8		dffun6	$⊢ Fun F \leftrightarrow (Rel F \land \forall x \exists^{*} y x F y)$
9	7 8	sylibr	$⊢ ((Rel F \land Rel G) \land Fun (F \cup G)) \to Fun F$
10		simpr	$⊢ (Rel F \land Rel G) \to Rel G$
11		uncom	$⊢ F \cup G = G \cup F$
12	11	funeqi	$⊢ Fun (F \cup G) \leftrightarrow Fun (G \cup F)$
13		fununmo	$⊢ Fun (G \cup F) \to \exists^{*} y x G y$
14	12 13	sylbi	$⊢ Fun (F \cup G) \to \exists^{*} y x G y$
15	14	alrimiv	$⊢ Fun (F \cup G) \to \forall x \exists^{*} y x G y$
16	10 15	anim12i	$⊢ ((Rel F \land Rel G) \land Fun (F \cup G)) \to (Rel G \land \forall x \exists^{*} y x G y)$
17		dffun6	$⊢ Fun G \leftrightarrow (Rel G \land \forall x \exists^{*} y x G y)$
18	16 17	sylibr	$⊢ ((Rel F \land Rel G) \land Fun (F \cup G)) \to Fun G$
19	9 18	jca	$⊢ ((Rel F \land Rel G) \land Fun (F \cup G)) \to (Fun F \land Fun G)$
20	3 19	mpancom	$⊢ Fun (F \cup G) \to (Fun F \land Fun G)$

Metamath Proof Explorer