isthincd

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

	Ref	Expression
Hypotheses	isthincd.b	$⊢ φ \to B = {Base}_{C}$
	isthincd.h	$⊢ φ \to H = Hom (C)$
	isthincd.t	$⊢ (φ \land (x \in B \land y \in B)) \to \exists^{*} f f \in (x H y)$
	isthincd.c	$⊢ φ \to C \in Cat$
Assertion	isthincd	Could not format assertion : No typesetting found for \|- ( ph -> C e. ThinCat ) with typecode \|-

Step	Hyp	Ref	Expression
1		isthincd.b	$⊢ φ \to B = {Base}_{C}$
2		isthincd.h	$⊢ φ \to H = Hom (C)$
3		isthincd.t	$⊢ (φ \land (x \in B \land y \in B)) \to \exists^{*} f f \in (x H y)$
4		isthincd.c	$⊢ φ \to C \in Cat$
5	3	ralrimivva	$⊢ φ \to \forall x \in B \forall y \in B \exists^{*} f f \in (x H y)$
6	2	oveqd	$⊢ φ \to x H y = x Hom (C) y$
7	6	eleq2d	$⊢ φ \to (f \in (x H y) \leftrightarrow f \in (x Hom (C) y))$
8	7	mobidv	$⊢ φ \to (\exists^{} f f \in (x H y) \leftrightarrow \exists^{} f f \in (x Hom (C) y))$
9	1 8	raleqbidv	$⊢ φ \to (\forall y \in B \exists^{} f f \in (x H y) \leftrightarrow \forall y \in {Base}_{C} \exists^{} f f \in (x Hom (C) y))$
10	1 9	raleqbidv	$⊢ φ \to (\forall x \in B \forall y \in B \exists^{} f f \in (x H y) \leftrightarrow \forall x \in {Base}_{C} \forall y \in {Base}_{C} \exists^{} f f \in (x Hom (C) y))$
11	5 10	mpbid	$⊢ φ \to \forall x \in {Base}_{C} \forall y \in {Base}_{C} \exists^{*} f f \in (x Hom (C) y)$
12		eqid	$⊢ {Base}_{C} = {Base}_{C}$
13		eqid	$⊢ Hom (C) = Hom (C)$
14	12 13	isthinc	Could not format ( C e. ThinCat <-> ( C e. Cat /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) ) ) : No typesetting found for \|- ( C e. ThinCat <-> ( C e. Cat /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) ) ) with typecode \|-
15	4 11 14	sylanbrc	Could not format ( ph -> C e. ThinCat ) : No typesetting found for \|- ( ph -> C e. ThinCat ) with typecode \|-

Metamath Proof Explorer