Theorem isthinc2

Description: A thin category is a category in which all hom-sets have cardinality less than or equal to the cardinality of 1o . (Contributed by Zhi Wang, 17-Sep-2024)

	Ref	Expression
Hypotheses	isthinc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	isthinc.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion	isthinc2	⊢ ( 𝐶 ∈ ThinCat ↔ ( 𝐶 ∈ Cat ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ≼ 1o ) )

Proof

Step	Hyp	Ref	Expression
1		isthinc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		isthinc.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3	1 2	isthinc	⊢ ( 𝐶 ∈ ThinCat ↔ ( 𝐶 ∈ Cat ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) )
4		modom2	⊢ ( ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ ( 𝑥 𝐻 𝑦 ) ≼ 1o )
5	4	2ralbii	⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ≼ 1o )
6	5	anbi2i	⊢ ( ( 𝐶 ∈ Cat ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) ↔ ( 𝐶 ∈ Cat ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ≼ 1o ) )
7	3 6	bitri	⊢ ( 𝐶 ∈ ThinCat ↔ ( 𝐶 ∈ Cat ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ≼ 1o ) )