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

Metamath Proof Explorer

Theorem thincciso3

Description: Categories isomorphic to a thin category are thin. Example 3.26(2) of Adamek p. 33. Note that "thincciso2.u" is redundant thanks to elbasfv . (Contributed by Zhi Wang, 18-Oct-2025)

		Ref	Expression
	Hypotheses	thincciso2.c	$⊢ C = CatCat (U)$
		thincciso2.b	$⊢ B = {Base}_{C}$
		thincciso2.u	$⊢ φ \to U \in V$
		thincciso2.x	$⊢ φ \to X \in B$
		thincciso2.y	$⊢ φ \to Y \in B$
		thincciso2.i	$⊢ I = Iso (C)$
		thincciso2.f	$⊢ φ \to F \in (X I Y)$
		thincciso3.xt	$⊢ φ \to X \in ThinCat$
	Assertion	thincciso3	$⊢ φ \to Y \in ThinCat$

Proof

Step	Hyp	Ref	Expression
1		thincciso2.c	$⊢ C = CatCat (U)$
2		thincciso2.b	$⊢ B = {Base}_{C}$
3		thincciso2.u	$⊢ φ \to U \in V$
4		thincciso2.x	$⊢ φ \to X \in B$
5		thincciso2.y	$⊢ φ \to Y \in B$
6		thincciso2.i	$⊢ I = Iso (C)$
7		thincciso2.f	$⊢ φ \to F \in (X I Y)$
8		thincciso3.xt	$⊢ φ \to X \in ThinCat$
9		eqid	$⊢ Inv (C) = Inv (C)$
10	1	catccat	$⊢ U \in V \to C \in Cat$
11	3 10	syl	$⊢ φ \to C \in Cat$
12	2 9 11 4 5 6	invf	$⊢ φ \to (X Inv (C) Y) : X I Y ⟶ Y I X$
13	12 7	ffvelcdmd	$⊢ φ \to (X Inv (C) Y) (F) \in (Y I X)$
14	1 2 3 5 4 6 13 8	thincciso2	$⊢ φ \to Y \in ThinCat$