Metamath Proof Explorer

Theorem isofnALT

Description: The function value of the function returning the isomorphisms of a category is a function over the Cartesian square of the base set of the category. (Contributed by AV, 5-Apr-2020) (Proof shortened by Zhi Wang, 3-Nov-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion isofnALT 
|- ( C e. Cat -> ( Iso ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )

Proof

Step Hyp Ref Expression
1 dmexg 
 |-  ( x e. _V -> dom x e. _V )
2 1 adantl 
 |-  ( ( C e. Cat /\ x e. _V ) -> dom x e. _V )
3 2 ralrimiva 
 |-  ( C e. Cat -> A. x e. _V dom x e. _V )
4 eqid 
 |-  ( x e. _V |-> dom x ) = ( x e. _V |-> dom x )
5 4 fnmpt 
 |-  ( A. x e. _V dom x e. _V -> ( x e. _V |-> dom x ) Fn _V )
6 3 5 syl 
 |-  ( C e. Cat -> ( x e. _V |-> dom x ) Fn _V )
7 invfn 
 |-  ( C e. Cat -> ( Inv ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
8 ssv 
 |-  ran ( Inv ` C ) C_ _V
9 8 a1i 
 |-  ( C e. Cat -> ran ( Inv ` C ) C_ _V )
10 fnco 
 |-  ( ( ( x e. _V |-> dom x ) Fn _V /\ ( Inv ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) /\ ran ( Inv ` C ) C_ _V ) -> ( ( x e. _V |-> dom x ) o. ( Inv ` C ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
11 6 7 9 10 syl3anc 
 |-  ( C e. Cat -> ( ( x e. _V |-> dom x ) o. ( Inv ` C ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
12 isofval 
 |-  ( C e. Cat -> ( Iso ` C ) = ( ( x e. _V |-> dom x ) o. ( Inv ` C ) ) )
13 12 fneq1d 
 |-  ( C e. Cat -> ( ( Iso ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> ( ( x e. _V |-> dom x ) o. ( Inv ` C ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) ) )
14 11 13 mpbird 
 |-  ( C e. Cat -> ( Iso ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )