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

Metamath Proof Explorer

Theorem catcisoi

Description: A functor is an isomorphism of categories only if it is full and faithful, and is a bijection on the objects. Remark 3.28(2) in Adamek p. 34. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses catcisoi.c 
|- C = ( CatCat ` U )
catcisoi.r 
|- R = ( Base ` X )
catcisoi.s 
|- S = ( Base ` Y )
catcisoi.i 
|- I = ( Iso ` C )
catcisoi.f 
|- ( ph -> F e. ( X I Y ) )
Assertion catcisoi 
|- ( ph -> ( F e. ( ( X Full Y ) i^i ( X Faith Y ) ) /\ ( 1st ` F ) : R -1-1-onto-> S ) )

Proof

Step Hyp Ref Expression
1 catcisoi.c 
 |-  C = ( CatCat ` U )
2 catcisoi.r 
 |-  R = ( Base ` X )
3 catcisoi.s 
 |-  S = ( Base ` Y )
4 catcisoi.i 
 |-  I = ( Iso ` C )
5 catcisoi.f 
 |-  ( ph -> F e. ( X I Y ) )
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 4 5 6 isorcl2 
 |-  ( ph -> ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) )
8 7 simpld 
 |-  ( ph -> X e. ( Base ` C ) )
9 1 6 elbasfv 
 |-  ( X e. ( Base ` C ) -> U e. _V )
10 8 9 syl 
 |-  ( ph -> U e. _V )
11 7 simprd 
 |-  ( ph -> Y e. ( Base ` C ) )
12 1 6 2 3 10 8 11 4 catciso 
 |-  ( ph -> ( F e. ( X I Y ) <-> ( F e. ( ( X Full Y ) i^i ( X Faith Y ) ) /\ ( 1st ` F ) : R -1-1-onto-> S ) ) )
13 5 12 mpbid 
 |-  ( ph -> ( F e. ( ( X Full Y ) i^i ( X Faith Y ) ) /\ ( 1st ` F ) : R -1-1-onto-> S ) )