This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )