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	|- ( ph -> U e. V )
	thincciso2.x	|- ( ph -> X e. B )
	thincciso2.y	|- ( ph -> Y e. B )
	thincciso2.i	|- I = ( Iso ` C )
	thincciso2.f	|- ( ph -> F e. ( X I Y ) )
	thincciso3.xt	|- ( ph -> X e. ThinCat )
Assertion	thincciso3	|- ( ph -> Y e. ThinCat )

Proof

Step	Hyp	Ref	Expression
1		thincciso2.c	|- C = ( CatCat ` U )
2		thincciso2.b	|- B = ( Base ` C )
3		thincciso2.u	|- ( ph -> U e. V )
4		thincciso2.x	|- ( ph -> X e. B )
5		thincciso2.y	|- ( ph -> Y e. B )
6		thincciso2.i	|- I = ( Iso ` C )
7		thincciso2.f	|- ( ph -> F e. ( X I Y ) )
8		thincciso3.xt	|- ( ph -> X e. ThinCat )
9		eqid	|- ( Inv ` C ) = ( Inv ` C )
10	1	catccat	|- ( U e. V -> C e. Cat )
11	3 10	syl	|- ( ph -> C e. Cat )
12	2 9 11 4 5 6	invf	|- ( ph -> ( X ( Inv ` C ) Y ) : ( X I Y ) --> ( Y I X ) )
13	12 7	ffvelcdmd	|- ( ph -> ( ( X ( Inv ` C ) Y ) ` F ) e. ( Y I X ) )
14	1 2 3 5 4 6 13 8	thincciso2	|- ( ph -> Y e. ThinCat )