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	|- ( ph -> A. x e. B A. y e. B ( x .<_ y <-> ( x H y ) =/= (/) ) )
	catprs.b	|- ( ph -> B = ( Base ` C ) )
	catprs.h	|- ( ph -> H = ( Hom ` C ) )
	catprs.c	|- ( ph -> C e. Cat )
	catprs2.l	|- ( ph -> .<_ = ( le ` C ) )
Assertion	catprs2	|- ( ph -> C e. Proset )

Proof

Step	Hyp	Ref	Expression
1		catprs.1	|- ( ph -> A. x e. B A. y e. B ( x .<_ y <-> ( x H y ) =/= (/) ) )
2		catprs.b	|- ( ph -> B = ( Base ` C ) )
3		catprs.h	|- ( ph -> H = ( Hom ` C ) )
4		catprs.c	|- ( ph -> C e. Cat )
5		catprs2.l	|- ( ph -> .<_ = ( le ` C ) )
6	1 2 3 4	catprs	|- ( ( ph /\ ( w e. B /\ v e. B /\ u e. B ) ) -> ( w .<_ w /\ ( ( w .<_ v /\ v .<_ u ) -> w .<_ u ) ) )
7	6	ralrimivvva	|- ( ph -> A. w e. B A. v e. B A. u e. B ( w .<_ w /\ ( ( w .<_ v /\ v .<_ u ) -> w .<_ u ) ) )
8	2 5 4	isprsd	|- ( ph -> ( C e. Proset <-> A. w e. B A. v e. B A. u e. B ( w .<_ w /\ ( ( w .<_ v /\ v .<_ u ) -> w .<_ u ) ) ) )
9	7 8	mpbird	|- ( ph -> C e. Proset )