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=\mathrm{CatCat}\left(U\right)$$
	catcisoi.r	$$⊢R={\mathrm{Base}}_X$$
	catcisoi.s	$$⊢S={\mathrm{Base}}_Y$$
	catcisoi.i	$$⊢I=\mathrm{Iso}\left(C\right)$$
	catcisoi.f	$$⊢\phi \to F\in \left(XIY\right)$$
Assertion	catcisoi	$$⊢\phi \to \left(F\in \left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)\wedge 1^{st}\left(F\right):R\underset{1-1\; onto}{⟶}S\right)$$

Proof

Step	Hyp	Ref	Expression
1		catcisoi.c	$$⊢C=\mathrm{CatCat}\left(U\right)$$
2		catcisoi.r	$$⊢R={\mathrm{Base}}_X$$
3		catcisoi.s	$$⊢S={\mathrm{Base}}_Y$$
4		catcisoi.i	$$⊢I=\mathrm{Iso}\left(C\right)$$
5		catcisoi.f	$$⊢\phi \to F\in \left(XIY\right)$$
6		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
7	4 5 6	isorcl2	$$⊢\phi \to \left(X\in {\mathrm{Base}}_C\wedge Y\in {\mathrm{Base}}_C\right)$$
8	7	simpld	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
9	1 6	elbasfv	$$⊢X\in {\mathrm{Base}}_C\to U\in \mathrm{V}$$
10	8 9	syl	$$⊢\phi \to U\in \mathrm{V}$$
11	7	simprd	$$⊢\phi \to Y\in {\mathrm{Base}}_C$$
12	1 6 2 3 10 8 11 4	catciso	$$⊢\phi \to \left(F\in \left(XIY\right)\leftrightarrow \left(F\in \left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)\wedge 1^{st}\left(F\right):R\underset{1-1\; onto}{⟶}S\right)\right)$$
13	5 12	mpbid	$$⊢\phi \to \left(F\in \left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)\wedge 1^{st}\left(F\right):R\underset{1-1\; onto}{⟶}S\right)$$