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

Metamath Proof Explorer

Theorem comfffn

Description: The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses comfffn.o 
|- O = ( comf ` C )
comfffn.b 
|- B = ( Base ` C )
Assertion comfffn 
|- O Fn ( ( B X. B ) X. B )

Proof

Step Hyp Ref Expression
1 comfffn.o 
 |-  O = ( comf ` C )
2 comfffn.b 
 |-  B = ( Base ` C )
3 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
4 eqid 
 |-  ( comp ` C ) = ( comp ` C )
5 1 2 3 4 comfffval 
 |-  O = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) ( Hom ` C ) y ) , f e. ( ( Hom ` C ) ` x ) |-> ( g ( x ( comp ` C ) y ) f ) ) )
6 ovex 
 |-  ( ( 2nd ` x ) ( Hom ` C ) y ) e. _V
7 fvex 
 |-  ( ( Hom ` C ) ` x ) e. _V
8 6 7 mpoex 
 |-  ( g e. ( ( 2nd ` x ) ( Hom ` C ) y ) , f e. ( ( Hom ` C ) ` x ) |-> ( g ( x ( comp ` C ) y ) f ) ) e. _V
9 5 8 fnmpoi 
 |-  O Fn ( ( B X. B ) X. B )