Theorem catprs2

Description: A category equipped with the induced preorder, where an object x is defined to be "less than or equal to" y iff there is a morphism from x to y , is a preordered set, or a proset. The category might not be thin. See catprsc and catprsc2 for constructions satisfying the hypothesis "catprs.1". See catprs for a more primitive version. See prsthinc for constructing a thin category from a proset. (Contributed by Zhi Wang, 18-Sep-2024)

	Ref	Expression
Hypotheses	catprs.1	$$⊢\phi \to \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow xHy\ne \varnothing \right)$$
	catprs.b	$$⊢\phi \to B={\mathrm{Base}}_C$$
	catprs.h	$$⊢\phi \to H=\mathrm{Hom}\left(C\right)$$
	catprs.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	catprs2.l	$$⊢\phi \to \underset{\dot{}}{\le }={\le }_C$$
Assertion	catprs2	$$⊢\phi \to C\in \mathrm{Proset}$$

Proof

Step	Hyp	Ref	Expression
1		catprs.1	$$⊢\phi \to \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow xHy\ne \varnothing \right)$$
2		catprs.b	$$⊢\phi \to B={\mathrm{Base}}_C$$
3		catprs.h	$$⊢\phi \to H=\mathrm{Hom}\left(C\right)$$
4		catprs.c	$$⊢\phi \to C\in \mathrm{Cat}$$
5		catprs2.l	$$⊢\phi \to \underset{\dot{}}{\le }={\le }_C$$
6	1 2 3 4	catprs	$$⊢\left(\phi \wedge \left(w\in B\wedge v\in B\wedge u\in B\right)\right)\to \left(w\underset{\dot{}}{\le }w\wedge \left(\left(w\underset{\dot{}}{\le }v\wedge v\underset{\dot{}}{\le }u\right)\to w\underset{\dot{}}{\le }u\right)\right)$$
7	6	ralrimivvva	$$⊢\phi \to \forall w\in B\forall v\in B\forall u\in B\left(w\underset{\dot{}}{\le }w\wedge \left(\left(w\underset{\dot{}}{\le }v\wedge v\underset{\dot{}}{\le }u\right)\to w\underset{\dot{}}{\le }u\right)\right)$$
8	2 5 4	isprsd	$$⊢\phi \to \left(C\in \mathrm{Proset}\leftrightarrow \forall w\in B\forall v\in B\forall u\in B\left(w\underset{\dot{}}{\le }w\wedge \left(\left(w\underset{\dot{}}{\le }v\wedge v\underset{\dot{}}{\le }u\right)\to w\underset{\dot{}}{\le }u\right)\right)\right)$$
9	7 8	mpbird	$$⊢\phi \to C\in \mathrm{Proset}$$