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	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
	thincciso2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	thincciso2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	thincciso2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	thincciso2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	thincciso2.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
	thincciso2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
	thincciso3.xt	⊢ ( 𝜑 → 𝑋 ∈ ThinCat )
Assertion	thincciso3	⊢ ( 𝜑 → 𝑌 ∈ ThinCat )

Proof

Step	Hyp	Ref	Expression
1		thincciso2.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2		thincciso2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		thincciso2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
4		thincciso2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		thincciso2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		thincciso2.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
7		thincciso2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
8		thincciso3.xt	⊢ ( 𝜑 → 𝑋 ∈ ThinCat )
9		eqid	⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
10	1	catccat	⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
11	3 10	syl	⊢ ( 𝜑 → 𝐶 ∈ Cat )
12	2 9 11 4 5 6	invf	⊢ ( 𝜑 → ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) : ( 𝑋 𝐼 𝑌 ) ⟶ ( 𝑌 𝐼 𝑋 ) )
13	12 7	ffvelcdmd	⊢ ( 𝜑 → ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 𝐼 𝑋 ) )
14	1 2 3 5 4 6 13 8	thincciso2	⊢ ( 𝜑 → 𝑌 ∈ ThinCat )