Metamath Proof Explorer

Theorem isofval

Description: Function value of the function returning the isomorphisms of a category. (Contributed by AV, 5-Apr-2017)

Ref Expression
Assertion isofval 
|- ( C e. Cat -> ( Iso ` C ) = ( ( x e. _V |-> dom x ) o. ( Inv ` C ) ) )

Proof

Step Hyp Ref Expression
1 df-iso 
 |-  Iso = ( c e. Cat |-> ( ( x e. _V |-> dom x ) o. ( Inv ` c ) ) )
2 fveq2 
 |-  ( c = C -> ( Inv ` c ) = ( Inv ` C ) )
3 2 coeq2d 
 |-  ( c = C -> ( ( x e. _V |-> dom x ) o. ( Inv ` c ) ) = ( ( x e. _V |-> dom x ) o. ( Inv ` C ) ) )
4 id 
 |-  ( C e. Cat -> C e. Cat )
5 funmpt 
 |-  Fun ( x e. _V |-> dom x )
6 fvexd 
 |-  ( C e. Cat -> ( Inv ` C ) e. _V )
7 cofunexg 
 |-  ( ( Fun ( x e. _V |-> dom x ) /\ ( Inv ` C ) e. _V ) -> ( ( x e. _V |-> dom x ) o. ( Inv ` C ) ) e. _V )
8 5 6 7 sylancr 
 |-  ( C e. Cat -> ( ( x e. _V |-> dom x ) o. ( Inv ` C ) ) e. _V )
9 1 3 4 8 fvmptd3 
 |-  ( C e. Cat -> ( Iso ` C ) = ( ( x e. _V |-> dom x ) o. ( Inv ` C ) ) )