Theorem isthinc3

Description: A thin category is a category in which, given a pair of objects x and y and any two morphisms f , g from x to y , the morphisms are equal. (Contributed by Zhi Wang, 17-Sep-2024)

	Ref	Expression
Hypotheses	isthinc.b	$$⊢B={\mathrm{Base}}_C$$
	isthinc.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
Assertion	isthinc3	Could not format assertion : No typesetting found for |- ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B A. f e. ( x H y ) A. g e. ( x H y ) f = g ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		isthinc.b	$$⊢B={\mathrm{Base}}_C$$
2		isthinc.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
3	1 2	isthinc	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 |-
4		moel	$$⊢{\exists }^{*}ff\in \left(xHy\right)\leftrightarrow \forall f\in \left(xHy\right)\forall g\in \left(xHy\right)f=g$$
5	4	2ralbii	$$⊢\forall x\in B\forall y\in B{\exists }^{*}ff\in \left(xHy\right)\leftrightarrow \forall x\in B\forall y\in B\forall f\in \left(xHy\right)\forall g\in \left(xHy\right)f=g$$
6	5	anbi2i	$$⊢\left(C\in \mathrm{Cat}\wedge \forall x\in B\forall y\in B{\exists }^{*}ff\in \left(xHy\right)\right)\leftrightarrow \left(C\in \mathrm{Cat}\wedge \forall x\in B\forall y\in B\forall f\in \left(xHy\right)\forall g\in \left(xHy\right)f=g\right)$$
7	3 6	bitri	Could not format ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B A. f e. ( x H y ) A. g e. ( x H y ) f = g ) ) : No typesetting found for |- ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B A. f e. ( x H y ) A. g e. ( x H y ) f = g ) ) with typecode |-