Theorem prstcprs

Description: The category is a preordered set. (Contributed by Zhi Wang, 20-Sep-2024)

	Ref	Expression
Hypotheses	prstcnid.c	|- ( ph -> C = ( ProsetToCat ` K ) )
	prstcnid.k	|- ( ph -> K e. Proset )
Assertion	prstcprs	|- ( ph -> C e. Proset )

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	|- ( ph -> C = ( ProsetToCat ` K ) )
2		prstcnid.k	|- ( ph -> K e. Proset )
3		eqidd	|- ( ph -> ( Base ` K ) = ( Base ` K ) )
4	1 2 3	prstcbas	|- ( ph -> ( Base ` K ) = ( Base ` C ) )
5		eqidd	|- ( ph -> ( le ` K ) = ( le ` K ) )
6	1 2 5	prstcleval	|- ( ph -> ( le ` K ) = ( le ` C ) )
7		fvex	|- ( ProsetToCat ` K ) e. _V
8	1 7	eqeltrdi	|- ( ph -> C e. _V )
9	4 6 8	isprsd	|- ( ph -> ( C e. Proset <-> A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
10	3 5 2	isprsd	|- ( ph -> ( K e. Proset <-> A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
11	9 10	bitr4d	|- ( ph -> ( C e. Proset <-> K e. Proset ) )
12	2 11	mpbird	|- ( ph -> C e. Proset )