This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 /\ 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 ) )