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	$⊢ φ \to F \in (X I Y)$
	Assertion	catcisoi	$⊢ φ \to (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{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	$⊢ φ \to F \in (X I Y)$
6		eqid	$⊢ {Base}_{C} = {Base}_{C}$
7	4 5 6	isorcl2	$⊢ φ \to (X \in {Base}_{C} \land Y \in {Base}_{C})$
8	7	simpld	$⊢ φ \to X \in {Base}_{C}$
9	1 6	elbasfv	$⊢ X \in {Base}_{C} \to U \in V$
10	8 9	syl	$⊢ φ \to U \in V$
11	7	simprd	$⊢ φ \to Y \in {Base}_{C}$
12	1 6 2 3 10 8 11 4	catciso	$⊢ φ \to (F \in (X I Y) \leftrightarrow (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S))$
13	5 12	mpbid	$⊢ φ \to (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S)$