Theorem setcthin

Description: A category of sets all of whose objects contain at most one element is thin. (Contributed by Zhi Wang, 20-Sep-2024)

	Ref	Expression
Hypotheses	setcthin.c	⊢ ( 𝜑 → 𝐶 = ( SetCat ‘ 𝑈 ) )
	setcthin.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	setcthin.x	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑈 ∃* 𝑝 𝑝 ∈ 𝑥 )
Assertion	setcthin	⊢ ( 𝜑 → 𝐶 ∈ ThinCat )

Proof

Step	Hyp	Ref	Expression
1		setcthin.c	⊢ ( 𝜑 → 𝐶 = ( SetCat ‘ 𝑈 ) )
2		setcthin.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3		setcthin.x	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑈 ∃* 𝑝 𝑝 ∈ 𝑥 )
4		eqid	⊢ ( SetCat ‘ 𝑈 ) = ( SetCat ‘ 𝑈 )
5	4 2	setcbas	⊢ ( 𝜑 → 𝑈 = ( Base ‘ ( SetCat ‘ 𝑈 ) ) )
6		eqidd	⊢ ( 𝜑 → ( Hom ‘ ( SetCat ‘ 𝑈 ) ) = ( Hom ‘ ( SetCat ‘ 𝑈 ) ) )
7		elequ2	⊢ ( 𝑥 = 𝑧 → ( 𝑝 ∈ 𝑥 ↔ 𝑝 ∈ 𝑧 ) )
8	7	mobidv	⊢ ( 𝑥 = 𝑧 → ( ∃* 𝑝 𝑝 ∈ 𝑥 ↔ ∃* 𝑝 𝑝 ∈ 𝑧 ) )
9	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) → ∀ 𝑥 ∈ 𝑈 ∃* 𝑝 𝑝 ∈ 𝑥 )
10		simprr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑧 ∈ 𝑈 )
11	8 9 10	rspcdva	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) → ∃* 𝑝 𝑝 ∈ 𝑧 )
12		mofmo	⊢ ( ∃* 𝑝 𝑝 ∈ 𝑧 → ∃* 𝑓 𝑓 : 𝑦 ⟶ 𝑧 )
13	11 12	syl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) → ∃* 𝑓 𝑓 : 𝑦 ⟶ 𝑧 )
14	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑈 ∈ 𝑉 )
15		eqid	⊢ ( Hom ‘ ( SetCat ‘ 𝑈 ) ) = ( Hom ‘ ( SetCat ‘ 𝑈 ) )
16		simprl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑦 ∈ 𝑈 )
17	4 14 15 16 10	elsetchom	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) → ( 𝑓 ∈ ( 𝑦 ( Hom ‘ ( SetCat ‘ 𝑈 ) ) 𝑧 ) ↔ 𝑓 : 𝑦 ⟶ 𝑧 ) )
18	17	mobidv	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) → ( ∃* 𝑓 𝑓 ∈ ( 𝑦 ( Hom ‘ ( SetCat ‘ 𝑈 ) ) 𝑧 ) ↔ ∃* 𝑓 𝑓 : 𝑦 ⟶ 𝑧 ) )
19	13 18	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑦 ( Hom ‘ ( SetCat ‘ 𝑈 ) ) 𝑧 ) )
20	4	setccat	⊢ ( 𝑈 ∈ 𝑉 → ( SetCat ‘ 𝑈 ) ∈ Cat )
21	2 20	syl	⊢ ( 𝜑 → ( SetCat ‘ 𝑈 ) ∈ Cat )
22	5 6 19 21	isthincd	⊢ ( 𝜑 → ( SetCat ‘ 𝑈 ) ∈ ThinCat )
23	1 22	eqeltrd	⊢ ( 𝜑 → 𝐶 ∈ ThinCat )