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 ) )