Theorem thincciso2

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)$$
	thincciso2.yt	$$⊢\phi \to Y\in \mathrm{ThinCat}$$
Assertion	thincciso2	$$⊢\phi \to X\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		thincciso2.yt	$$⊢\phi \to Y\in \mathrm{ThinCat}$$
9		eqidd	$$⊢\phi \to {\mathrm{Base}}_X={\mathrm{Base}}_X$$
10		eqidd	$$⊢\phi \to \mathrm{Hom}\left(X\right)=\mathrm{Hom}\left(X\right)$$
11		relfull	$$⊢\mathrm{Rel}\left(X\mathrm{Full}Y\right)$$
12		relin1	$$⊢\mathrm{Rel}\left(X\mathrm{Full}Y\right)\to \mathrm{Rel}\left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)$$
13	11 12	ax-mp	$$⊢\mathrm{Rel}\left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)$$
14		eqid	$$⊢{\mathrm{Base}}_X={\mathrm{Base}}_X$$
15		eqid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
16	1 2 14 15 3 4 5 6	catciso	$$⊢\phi \to \left(F\in \left(XIY\right)\leftrightarrow \left(F\in \left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)\wedge 1^{st}\left(F\right):{\mathrm{Base}}_X\underset{1-1\; onto}{⟶}{\mathrm{Base}}_Y\right)\right)$$
17	7 16	mpbid	$$⊢\phi \to \left(F\in \left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)\wedge 1^{st}\left(F\right):{\mathrm{Base}}_X\underset{1-1\; onto}{⟶}{\mathrm{Base}}_Y\right)$$
18	17	simpld	$$⊢\phi \to F\in \left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)$$
19		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)\wedge F\in \left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)\right)\to 1^{st}\left(F\right)\left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)2^{nd}\left(F\right)$$
20	13 18 19	sylancr	$$⊢\phi \to 1^{st}\left(F\right)\left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)2^{nd}\left(F\right)$$
21		eqid	$$⊢\mathrm{Hom}\left(X\right)=\mathrm{Hom}\left(X\right)$$
22		eqid	$$⊢\mathrm{Hom}\left(Y\right)=\mathrm{Hom}\left(Y\right)$$
23	14 21 22	isffth2	$$⊢1^{st}\left(F\right)\left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)2^{nd}\left(F\right)\leftrightarrow \left(1^{st}\left(F\right)\left(X\mathrm{Func}Y\right)2^{nd}\left(F\right)\wedge \forall x\in {\mathrm{Base}}_X\forall y\in {\mathrm{Base}}_X\left(x{2}^{nd}\left(F\right)y\right):x\mathrm{Hom}\left(X\right)y\underset{1-1\; onto}{⟶}{1}^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(Y\right)1^{st}\left(F\right)\left(y\right)\right)$$
24	20 23	sylib	$$⊢\phi \to \left(1^{st}\left(F\right)\left(X\mathrm{Func}Y\right)2^{nd}\left(F\right)\wedge \forall x\in {\mathrm{Base}}_X\forall y\in {\mathrm{Base}}_X\left(x{2}^{nd}\left(F\right)y\right):x\mathrm{Hom}\left(X\right)y\underset{1-1\; onto}{⟶}{1}^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(Y\right)1^{st}\left(F\right)\left(y\right)\right)$$
25	24	simprd	$$⊢\phi \to \forall x\in {\mathrm{Base}}_X\forall y\in {\mathrm{Base}}_X\left(x{2}^{nd}\left(F\right)y\right):x\mathrm{Hom}\left(X\right)y\underset{1-1\; onto}{⟶}{1}^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(Y\right)1^{st}\left(F\right)\left(y\right)$$
26	25	r19.21bi	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_X\right)\to \forall y\in {\mathrm{Base}}_X\left(x{2}^{nd}\left(F\right)y\right):x\mathrm{Hom}\left(X\right)y\underset{1-1\; onto}{⟶}{1}^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(Y\right)1^{st}\left(F\right)\left(y\right)$$
27	26	r19.21bi	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_X\right)\wedge y\in {\mathrm{Base}}_X\right)\to \left(x{2}^{nd}\left(F\right)y\right):x\mathrm{Hom}\left(X\right)y\underset{1-1\; onto}{⟶}{1}^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(Y\right)1^{st}\left(F\right)\left(y\right)$$
28	27	anasss	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_X\wedge y\in {\mathrm{Base}}_X\right)\right)\to \left(x{2}^{nd}\left(F\right)y\right):x\mathrm{Hom}\left(X\right)y\underset{1-1\; onto}{⟶}{1}^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(Y\right)1^{st}\left(F\right)\left(y\right)$$
29		ovex	$$⊢x\mathrm{Hom}\left(X\right)y\in \mathrm{V}$$
30	29	f1oen	$$⊢\left(x{2}^{nd}\left(F\right)y\right):x\mathrm{Hom}\left(X\right)y\underset{1-1\; onto}{⟶}{1}^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(Y\right)1^{st}\left(F\right)\left(y\right)\to \left(x\mathrm{Hom}\left(X\right)y\right)\approx \left(1^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(Y\right)1^{st}\left(F\right)\left(y\right)\right)$$
31	28 30	syl	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_X\wedge y\in {\mathrm{Base}}_X\right)\right)\to \left(x\mathrm{Hom}\left(X\right)y\right)\approx \left(1^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(Y\right)1^{st}\left(F\right)\left(y\right)\right)$$
32	8	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_X\wedge y\in {\mathrm{Base}}_X\right)\right)\to Y\in \mathrm{ThinCat}$$
33	24	simpld	$$⊢\phi \to 1^{st}\left(F\right)\left(X\mathrm{Func}Y\right)2^{nd}\left(F\right)$$
34	14 15 33	funcf1	$$⊢\phi \to 1^{st}\left(F\right):{\mathrm{Base}}_X⟶{\mathrm{Base}}_Y$$
35	34	ffvelcdmda	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_X\right)\to 1^{st}\left(F\right)\left(x\right)\in {\mathrm{Base}}_Y$$
36	35	adantrr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_X\wedge y\in {\mathrm{Base}}_X\right)\right)\to 1^{st}\left(F\right)\left(x\right)\in {\mathrm{Base}}_Y$$
37	34	ffvelcdmda	$$⊢\left(\phi \wedge y\in {\mathrm{Base}}_X\right)\to 1^{st}\left(F\right)\left(y\right)\in {\mathrm{Base}}_Y$$
38	37	adantrl	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_X\wedge y\in {\mathrm{Base}}_X\right)\right)\to 1^{st}\left(F\right)\left(y\right)\in {\mathrm{Base}}_Y$$
39	32 36 38 15 22	thincmo	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_X\wedge y\in {\mathrm{Base}}_X\right)\right)\to {\exists }^{*}ff\in \left(1^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(Y\right)1^{st}\left(F\right)\left(y\right)\right)$$
40		modom2	$$⊢{\exists }^{*}ff\in \left(1^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(Y\right)1^{st}\left(F\right)\left(y\right)\right)\leftrightarrow \left(1^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(Y\right)1^{st}\left(F\right)\left(y\right)\right)\preccurlyeq 1_{𝑜}$$
41	39 40	sylib	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_X\wedge y\in {\mathrm{Base}}_X\right)\right)\to \left(1^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(Y\right)1^{st}\left(F\right)\left(y\right)\right)\preccurlyeq 1_{𝑜}$$
42		endomtr	$$⊢\left(\left(x\mathrm{Hom}\left(X\right)y\right)\approx \left(1^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(Y\right)1^{st}\left(F\right)\left(y\right)\right)\wedge \left(1^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(Y\right)1^{st}\left(F\right)\left(y\right)\right)\preccurlyeq 1_{𝑜}\right)\to \left(x\mathrm{Hom}\left(X\right)y\right)\preccurlyeq 1_{𝑜}$$
43	31 41 42	syl2anc	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_X\wedge y\in {\mathrm{Base}}_X\right)\right)\to \left(x\mathrm{Hom}\left(X\right)y\right)\preccurlyeq 1_{𝑜}$$
44		modom2	$$⊢{\exists }^{*}ff\in \left(x\mathrm{Hom}\left(X\right)y\right)\leftrightarrow \left(x\mathrm{Hom}\left(X\right)y\right)\preccurlyeq 1_{𝑜}$$
45	43 44	sylibr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_X\wedge y\in {\mathrm{Base}}_X\right)\right)\to {\exists }^{*}ff\in \left(x\mathrm{Hom}\left(X\right)y\right)$$
46	33	funcrcl2	$$⊢\phi \to X\in \mathrm{Cat}$$
47	9 10 45 46	isthincd	$$⊢\phi \to X\in \mathrm{ThinCat}$$