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 /\ Fun G ) -> Fun ( F o. G ) )

Proof

Step	Hyp	Ref	Expression
1		funmo	|- ( Fun G -> E* z x G z )
2		funmo	|- ( Fun F -> E* y z F y )
3	2	alrimiv	|- ( Fun F -> A. z E* y z F y )
4		moexexvw	|- ( ( E* z x G z /\ A. z E* y z F y ) -> E* y E. z ( x G z /\ z F y ) )
5	1 3 4	syl2anr	|- ( ( Fun F /\ Fun G ) -> E* y E. z ( x G z /\ z F y ) )
6	5	alrimiv	|- ( ( Fun F /\ Fun G ) -> A. x E* y E. z ( x G z /\ z F y ) )
7		funopab	|- ( Fun { <. x , y >. | E. z ( x G z /\ z F y ) } <-> A. x E* y E. z ( x G z /\ z F y ) )
8	6 7	sylibr	|- ( ( Fun F /\ Fun G ) -> Fun { <. x , y >. | E. z ( x G z /\ z F y ) } )
9		df-co	|- ( F o. G ) = { <. x , y >. | E. z ( x G z /\ z F y ) }
10	9	funeqi	|- ( Fun ( F o. G ) <-> Fun { <. x , y >. | E. z ( x G z /\ z F y ) } )
11	8 10	sylibr	|- ( ( Fun F /\ Fun G ) -> Fun ( F o. G ) )