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 ⊢ φ → C = SetCat ⁡ U
setcthin.u ⊢ φ → U ∈ V
setcthin.x ⊢ φ → ∀ x ∈ U ∃* p p ∈ x
Assertion setcthin ⊢ φ → C ∈ ThinCat

Proof

Step Hyp Ref Expression
1 setcthin.c ⊢ φ → C = SetCat ⁡ U
2 setcthin.u ⊢ φ → U ∈ V
3 setcthin.x ⊢ φ → ∀ x ∈ U ∃* p p ∈ x
4 eqid ⊢ SetCat ⁡ U = SetCat ⁡ U
5 4 2 setcbas ⊢ φ → U = Base SetCat ⁡ U
6 eqidd ⊢ φ → Hom ⁡ SetCat ⁡ U = Hom ⁡ SetCat ⁡ U
7 elequ2 ⊢ x = z → p ∈ x ↔ p ∈ z
8 7 mobidv ⊢ x = z → ∃* p p ∈ x ↔ ∃* p p ∈ z
9 3 adantr ⊢ φ ∧ y ∈ U ∧ z ∈ U → ∀ x ∈ U ∃* p p ∈ x
10 simprr ⊢ φ ∧ y ∈ U ∧ z ∈ U → z ∈ U
11 8 9 10 rspcdva ⊢ φ ∧ y ∈ U ∧ z ∈ U → ∃* p p ∈ z
12 mofmo ⊢ ∃* p p ∈ z → ∃* f f : y ⟶ z
13 11 12 syl ⊢ φ ∧ y ∈ U ∧ z ∈ U → ∃* f f : y ⟶ z
14 2 adantr ⊢ φ ∧ y ∈ U ∧ z ∈ U → U ∈ V
15 eqid ⊢ Hom ⁡ SetCat ⁡ U = Hom ⁡ SetCat ⁡ U
16 simprl ⊢ φ ∧ y ∈ U ∧ z ∈ U → y ∈ U
17 4 14 15 16 10 elsetchom ⊢ φ ∧ y ∈ U ∧ z ∈ U → f ∈ y Hom ⁡ SetCat ⁡ U z ↔ f : y ⟶ z
18 17 mobidv ⊢ φ ∧ y ∈ U ∧ z ∈ U → ∃* f f ∈ y Hom ⁡ SetCat ⁡ U z ↔ ∃* f f : y ⟶ z
19 13 18 mpbird ⊢ φ ∧ y ∈ U ∧ z ∈ U → ∃* f f ∈ y Hom ⁡ SetCat ⁡ U z
20 4 setccat ⊢ U ∈ V → SetCat ⁡ U ∈ Cat
21 2 20 syl ⊢ φ → SetCat ⁡ U ∈ Cat
22 5 6 19 21 isthincd ⊢ φ → SetCat ⁡ U ∈ ThinCat
23 1 22 eqeltrd ⊢ φ → C ∈ ThinCat