Metamath Proof Explorer

Theorem isthincd

Description: The predicate "is a thin category" (deduction form). (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Hypotheses isthincd.b ⊢ φ → B = Base C
isthincd.h ⊢ φ → H = Hom ⁡ C
isthincd.t ⊢ φ ∧ x ∈ B ∧ y ∈ B → ∃* f f ∈ x H y
isthincd.c ⊢ φ → C ∈ Cat
Assertion isthincd ⊢ φ → C ∈ ThinCat

Proof

Step Hyp Ref Expression
1 isthincd.b ⊢ φ → B = Base C
2 isthincd.h ⊢ φ → H = Hom ⁡ C
3 isthincd.t ⊢ φ ∧ x ∈ B ∧ y ∈ B → ∃* f f ∈ x H y
4 isthincd.c ⊢ φ → C ∈ Cat
5 3 ralrimivva ⊢ φ → ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y
6 2 oveqd ⊢ φ → x H y = x Hom ⁡ C y
7 6 eleq2d ⊢ φ → f ∈ x H y ↔ f ∈ x Hom ⁡ C y
8 7 mobidv ⊢ φ → ∃* f f ∈ x H y ↔ ∃* f f ∈ x Hom ⁡ C y
9 1 8 raleqbidv ⊢ φ → ∀ y ∈ B ∃* f f ∈ x H y ↔ ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ C y
10 1 9 raleqbidv ⊢ φ → ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y ↔ ∀ x ∈ Base C ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ C y
11 5 10 mpbid ⊢ φ → ∀ x ∈ Base C ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ C y
12 eqid ⊢ Base C = Base C
13 eqid ⊢ Hom ⁡ C = Hom ⁡ C
14 12 13 isthinc ⊢ C ∈ ThinCat ↔ C ∈ Cat ∧ ∀ x ∈ Base C ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ C y
15 4 11 14 sylanbrc ⊢ φ → C ∈ ThinCat