Theorem isthinc2

Description: A thin category is a category in which all hom-sets have cardinality less than or equal to the cardinality of 1o . (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	isthinc2	Could not format assertion : No typesetting found for |- ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B ( x H y ) ~<_ 1o ) ) 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		modom2	$$⊢{\exists }^{*}ff\in \left(xHy\right)\leftrightarrow \left(xHy\right)\preccurlyeq 1_{𝑜}$$
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\left(xHy\right)\preccurlyeq 1_{𝑜}$$
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\left(xHy\right)\preccurlyeq 1_{𝑜}\right)$$
7	3 6	bitri	Could not format ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B ( x H y ) ~<_ 1o ) ) : No typesetting found for |- ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B ( x H y ) ~<_ 1o ) ) with typecode |-