Theorem discthin

Description: A discrete category (a category whose only morphisms are the identity morphisms) is thin. (Contributed by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Hypotheses	discthin.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ }
	discthin.c	⊢ 𝐶 = ( ProsetToCat ‘ 𝐾 )
Assertion	discthin	⊢ ( 𝐵 ∈ 𝑉 → 𝐶 ∈ ThinCat )

Proof

Step	Hyp	Ref	Expression
1		discthin.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ }
2		discthin.c	⊢ 𝐶 = ( ProsetToCat ‘ 𝐾 )
3	2	a1i	⊢ ( 𝐵 ∈ 𝑉 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
4	1	resipos	⊢ ( 𝐵 ∈ 𝑉 → 𝐾 ∈ Poset )
5		posprs	⊢ ( 𝐾 ∈ Poset → 𝐾 ∈ Proset )
6	4 5	syl	⊢ ( 𝐵 ∈ 𝑉 → 𝐾 ∈ Proset )
7	3 6	prstcthin	⊢ ( 𝐵 ∈ 𝑉 → 𝐶 ∈ ThinCat )