Metamath Proof Explorer


Theorem prstcprs

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

Ref Expression
Hypotheses prstcnid.c No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
prstcnid.k φKProset
Assertion prstcprs φCProset

Proof

Step Hyp Ref Expression
1 prstcnid.c Could not format ( ph -> C = ( ProsetToCat ` K ) ) : No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
2 prstcnid.k φKProset
3 eqidd φBaseK=BaseK
4 1 2 3 prstcbas φBaseK=BaseC
5 eqidd φK=K
6 1 2 5 prstcleval φK=C
7 fvex Could not format ( ProsetToCat ` K ) e. _V : No typesetting found for |- ( ProsetToCat ` K ) e. _V with typecode |-
8 1 7 eqeltrdi φCV
9 4 6 8 isprsd φCProsetxBaseKyBaseKzBaseKxKxxKyyKzxKz
10 3 5 2 isprsd φKProsetxBaseKyBaseKzBaseKxKxxKyyKzxKz
11 9 10 bitr4d φCProsetKProset
12 2 11 mpbird φCProset