Metamath Proof Explorer

Theorem comffn

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 )
comffn.h 
|- H = ( Hom ` C )
comffn.x 
|- ( ph -> X e. B )
comffn.y 
|- ( ph -> Y e. B )
comffn.z 
|- ( ph -> Z e. B )
Assertion comffn 
|- ( ph -> ( <. X , Y >. O Z ) Fn ( ( Y H Z ) X. ( X H Y ) ) )

Proof

Step Hyp Ref Expression
1 comfffn.o 
 |-  O = ( comf ` C )
2 comfffn.b 
 |-  B = ( Base ` C )
3 comffn.h 
 |-  H = ( Hom ` C )
4 comffn.x 
 |-  ( ph -> X e. B )
5 comffn.y 
 |-  ( ph -> Y e. B )
6 comffn.z 
 |-  ( ph -> Z e. B )
7 eqid 
 |-  ( g e. ( Y H Z ) , f e. ( X H Y ) |-> ( g ( <. X , Y >. ( comp ` C ) Z ) f ) ) = ( g e. ( Y H Z ) , f e. ( X H Y ) |-> ( g ( <. X , Y >. ( comp ` C ) Z ) f ) )
8 ovex 
 |-  ( g ( <. X , Y >. ( comp ` C ) Z ) f ) e. _V
9 7 8 fnmpoi 
 |-  ( g e. ( Y H Z ) , f e. ( X H Y ) |-> ( g ( <. X , Y >. ( comp ` C ) Z ) f ) ) Fn ( ( Y H Z ) X. ( X H Y ) )
10 eqid 
 |-  ( comp ` C ) = ( comp ` C )
11 1 2 3 10 4 5 6 comffval 
 |-  ( ph -> ( <. X , Y >. O Z ) = ( g e. ( Y H Z ) , f e. ( X H Y ) |-> ( g ( <. X , Y >. ( comp ` C ) Z ) f ) ) )
12 11 fneq1d 
 |-  ( ph -> ( ( <. X , Y >. O Z ) Fn ( ( Y H Z ) X. ( X H Y ) ) <-> ( g e. ( Y H Z ) , f e. ( X H Y ) |-> ( g ( <. X , Y >. ( comp ` C ) Z ) f ) ) Fn ( ( Y H Z ) X. ( X H Y ) ) ) )
13 9 12 mpbiri 
 |-  ( ph -> ( <. X , Y >. O Z ) Fn ( ( Y H Z ) X. ( X H Y ) ) )