Metamath Proof Explorer

Theorem isthinc

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

Ref Expression
Hypotheses isthinc.b ⊢ B = Base C
isthinc.h ⊢ H = Hom ⁡ C
Assertion isthinc ⊢ C ∈ ThinCat ↔ C ∈ Cat ∧ ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y

Proof

Step Hyp Ref Expression
1 isthinc.b ⊢ B = Base C
2 isthinc.h ⊢ H = Hom ⁡ C
3 fvexd ⊢ c = C → Base c ∈ V
4 fveq2 ⊢ c = C → Base c = Base C
5 4 1 eqtr4di ⊢ c = C → Base c = B
6 fvexd ⊢ c = C ∧ b = B → Hom ⁡ c ∈ V
7 fveq2 ⊢ c = C → Hom ⁡ c = Hom ⁡ C
8 7 2 eqtr4di ⊢ c = C → Hom ⁡ c = H
9 8 adantr ⊢ c = C ∧ b = B → Hom ⁡ c = H
10 raleq ⊢ b = B → ∀ y ∈ b ∃* f f ∈ x h y ↔ ∀ y ∈ B ∃* f f ∈ x h y
11 10 raleqbi1dv ⊢ b = B → ∀ x ∈ b ∀ y ∈ b ∃* f f ∈ x h y ↔ ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x h y
12 11 ad2antlr ⊢ c = C ∧ b = B ∧ h = H → ∀ x ∈ b ∀ y ∈ b ∃* f f ∈ x h y ↔ ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x h y
13 oveq ⊢ h = H → x h y = x H y
14 13 eleq2d ⊢ h = H → f ∈ x h y ↔ f ∈ x H y
15 14 mobidv ⊢ h = H → ∃* f f ∈ x h y ↔ ∃* f f ∈ x H y
16 15 2ralbidv ⊢ h = H → ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x h y ↔ ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y
17 16 adantl ⊢ c = C ∧ b = B ∧ h = H → ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x h y ↔ ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y
18 12 17 bitrd ⊢ c = C ∧ b = B ∧ h = H → ∀ x ∈ b ∀ y ∈ b ∃* f f ∈ x h y ↔ ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y
19 6 9 18 sbcied2 ⊢ c = C ∧ b = B → [˙ Hom ⁡ c / h]˙ ∀ x ∈ b ∀ y ∈ b ∃* f f ∈ x h y ↔ ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y
20 3 5 19 sbcied2 ⊢ c = C → [˙Base c / b]˙ [˙ Hom ⁡ c / h]˙ ∀ x ∈ b ∀ y ∈ b ∃* f f ∈ x h y ↔ ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y
21 df-thinc ⊢ ThinCat = c ∈ Cat | [˙Base c / b]˙ [˙ Hom ⁡ c / h]˙ ∀ x ∈ b ∀ y ∈ b ∃* f f ∈ x h y
22 20 21 elrab2 ⊢ C ∈ ThinCat ↔ C ∈ Cat ∧ ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y