Metamath Proof Explorer

Theorem funco

Description: The composition of two functions is a function. Exercise 29 of TakeutiZaring p. 25. (Contributed by NM, 26-Jan-1997) (Proof shortened by Andrew Salmon, 17-Sep-2011)

		Ref	Expression
	Assertion	funco	$⊢ (Fun F \land Fun G) \to Fun (F \circ G)$

Proof

Step	Hyp	Ref	Expression
1		funmo	$⊢ Fun G \to \exists^{*} z x G z$
2		funmo	$⊢ Fun F \to \exists^{*} y z F y$
3	2	alrimiv	$⊢ Fun F \to \forall z \exists^{*} y z F y$
4		moexexvw	$⊢ (\exists^{} z x G z \land \forall z \exists^{} y z F y) \to \exists^{*} y \exists z (x G z \land z F y)$
5	1 3 4	syl2anr	$⊢ (Fun F \land Fun G) \to \exists^{*} y \exists z (x G z \land z F y)$
6	5	alrimiv	$⊢ (Fun F \land Fun G) \to \forall x \exists^{*} y \exists z (x G z \land z F y)$
7		funopab	$⊢ Fun \{⟨x, y⟩ \| \exists z (x G z \land z F y)\} \leftrightarrow \forall x \exists^{*} y \exists z (x G z \land z F y)$
8	6 7	sylibr	$⊢ (Fun F \land Fun G) \to Fun \{⟨x, y⟩ \| \exists z (x G z \land z F y)\}$
9		df-co	$⊢ F \circ G = \{⟨x, y⟩ \| \exists z (x G z \land z F y)\}$
10	9	funeqi	$⊢ Fun (F \circ G) \leftrightarrow Fun \{⟨x, y⟩ \| \exists z (x G z \land z F y)\}$
11	8 10	sylibr	$⊢ (Fun F \land Fun G) \to Fun (F \circ G)$