Metamath Proof Explorer

Theorem cidfn

Description: The identity arrow operator is a function from objects to arrows. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses cidfn.b 
|- B = ( Base ` C )
cidfn.i 
|- .1. = ( Id ` C )
Assertion cidfn 
|- ( C e. Cat -> .1. Fn B )

Proof

Step Hyp Ref Expression
1 cidfn.b 
 |-  B = ( Base ` C )
2 cidfn.i 
 |-  .1. = ( Id ` C )
3 riotaex 
 |-  ( iota_ g e. ( x ( Hom ` C ) x ) A. y e. B ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) e. _V
4 eqid 
 |-  ( x e. B |-> ( iota_ g e. ( x ( Hom ` C ) x ) A. y e. B ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) ) = ( x e. B |-> ( iota_ g e. ( x ( Hom ` C ) x ) A. y e. B ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) )
5 3 4 fnmpti 
 |-  ( x e. B |-> ( iota_ g e. ( x ( Hom ` C ) x ) A. y e. B ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) ) Fn B
6 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
7 eqid 
 |-  ( comp ` C ) = ( comp ` C )
8 id 
 |-  ( C e. Cat -> C e. Cat )
9 1 6 7 8 2 cidfval 
 |-  ( C e. Cat -> .1. = ( x e. B |-> ( iota_ g e. ( x ( Hom ` C ) x ) A. y e. B ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) ) )
10 9 fneq1d 
 |-  ( C e. Cat -> ( .1. Fn B <-> ( x e. B |-> ( iota_ g e. ( x ( Hom ` C ) x ) A. y e. B ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) ) Fn B ) )
11 5 10 mpbiri 
 |-  ( C e. Cat -> .1. Fn B )