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 Could not format assertion : No typesetting found for |- ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) ) with typecode |-

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 Could not format ThinCat = { c e. Cat | [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. A. x e. b A. y e. b E* f f e. ( x h y ) } : No typesetting found for |- ThinCat = { c e. Cat | [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. A. x e. b A. y e. b E* f f e. ( x h y ) } with typecode |-
22 20 21 elrab2 Could not format ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) ) : No typesetting found for |- ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) ) with typecode |-