Metamath Proof Explorer

Theorem 0thincg

Description: Any structure with an empty set of objects is a thin category. (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Assertion 0thincg ⊢ C ∈ V ∧ ∅ = Base C → C ∈ ThinCat

Proof

Step Hyp Ref Expression
1 0catg ⊢ C ∈ V ∧ ∅ = Base C → C ∈ Cat
2 ral0 ⊢ ∀ x ∈ ∅ ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ C y
3 raleq ⊢ ∅ = Base C → ∀ x ∈ ∅ ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ C y ↔ ∀ x ∈ Base C ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ C y
4 2 3 mpbii ⊢ ∅ = Base C → ∀ x ∈ Base C ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ C y
5 4 adantl ⊢ C ∈ V ∧ ∅ = Base C → ∀ x ∈ Base C ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ C y
6 eqid ⊢ Base C = Base C
7 eqid ⊢ Hom ⁡ C = Hom ⁡ C
8 6 7 isthinc ⊢ C ∈ ThinCat ↔ C ∈ Cat ∧ ∀ x ∈ Base C ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ C y
9 1 5 8 sylanbrc ⊢ C ∈ V ∧ ∅ = Base C → C ∈ ThinCat