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=\mathrm{CatCat}\left(U\right)$$
	thincciso2.b	$$⊢B={\mathrm{Base}}_C$$
	thincciso2.u	$$⊢\phi \to U\in V$$
	thincciso2.x	$$⊢\phi \to X\in B$$
	thincciso2.y	$$⊢\phi \to Y\in B$$
	thincciso2.i	$$⊢I=\mathrm{Iso}\left(C\right)$$
	thincciso2.f	$$⊢\phi \to F\in \left(XIY\right)$$
	thincciso3.xt	$$⊢\phi \to X\in \mathrm{ThinCat}$$
Assertion	thincciso3	$$⊢\phi \to Y\in \mathrm{ThinCat}$$

Proof

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