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	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
	thincciso2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	thincciso2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	thincciso2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	thincciso2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	thincciso2.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
	thincciso2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
	thincciso2.yt	⊢ ( 𝜑 → 𝑌 ∈ ThinCat )
Assertion	thincciso2	⊢ ( 𝜑 → 𝑋 ∈ 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		thincciso2.yt	⊢ ( 𝜑 → 𝑌 ∈ ThinCat )
9		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 ) )
10		eqidd	⊢ ( 𝜑 → ( Hom ‘ 𝑋 ) = ( Hom ‘ 𝑋 ) )
11		relfull	⊢ Rel ( 𝑋 Full 𝑌 )
12		relin1	⊢ ( Rel ( 𝑋 Full 𝑌 ) → Rel ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) )
13	11 12	ax-mp	⊢ Rel ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) )
14		eqid	⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
15		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
16	1 2 14 15 3 4 5 6	catciso	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ) )
17	7 16	mpbid	⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) )
18	17	simpld	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) )
19		1st2ndbr	⊢ ( ( Rel ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ) → ( 1^st ‘ 𝐹 ) ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ( 2^nd ‘ 𝐹 ) )
20	13 18 19	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ( 2^nd ‘ 𝐹 ) )
21		eqid	⊢ ( Hom ‘ 𝑋 ) = ( Hom ‘ 𝑋 )
22		eqid	⊢ ( Hom ‘ 𝑌 ) = ( Hom ‘ 𝑌 )
23	14 21 22	isffth2	⊢ ( ( 1^st ‘ 𝐹 ) ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ( 2^nd ‘ 𝐹 ) ↔ ( ( 1^st ‘ 𝐹 ) ( 𝑋 Func 𝑌 ) ( 2^nd ‘ 𝐹 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑋 ) ∀ 𝑦 ∈ ( Base ‘ 𝑋 ) ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) –1-1-onto→ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
24	20 23	sylib	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ( 𝑋 Func 𝑌 ) ( 2^nd ‘ 𝐹 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑋 ) ∀ 𝑦 ∈ ( Base ‘ 𝑋 ) ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) –1-1-onto→ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
25	24	simprd	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑋 ) ∀ 𝑦 ∈ ( Base ‘ 𝑋 ) ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) –1-1-onto→ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
26	25	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑋 ) ) → ∀ 𝑦 ∈ ( Base ‘ 𝑋 ) ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) –1-1-onto→ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
27	26	r19.21bi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) –1-1-onto→ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
28	27	anasss	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) –1-1-onto→ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
29		ovex	⊢ ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) ∈ V
30	29	f1oen	⊢ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) –1-1-onto→ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) → ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) ≈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
31	28 30	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) ≈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
32	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → 𝑌 ∈ ThinCat )
33	24	simpld	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝑋 Func 𝑌 ) ( 2^nd ‘ 𝐹 ) )
34	14 15 33	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) )
35	34	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑋 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑌 ) )
36	35	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑌 ) )
37	34	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑌 ) )
38	37	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑌 ) )
39	32 36 38 15 22	thincmo	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ∃* 𝑓 𝑓 ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
40		modom2	⊢ ( ∃* 𝑓 𝑓 ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ↔ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ≼ 1_o )
41	39 40	sylib	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ≼ 1_o )
42		endomtr	⊢ ( ( ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) ≈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∧ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ≼ 1_o ) → ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) ≼ 1_o )
43	31 41 42	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) ≼ 1_o )
44		modom2	⊢ ( ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) ↔ ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) ≼ 1_o )
45	43 44	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ∧ 𝑦 ∈ ( Base ‘ 𝑋 ) ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) )
46	33	funcrcl2	⊢ ( 𝜑 → 𝑋 ∈ Cat )
47	9 10 45 46	isthincd	⊢ ( 𝜑 → 𝑋 ∈ ThinCat )

Metamath Proof Explorer

Theorem thincciso2

Proof