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 | |
||
Assertion | prstcprs | |
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 | |
|
3 | eqidd | |
|
4 | 1 2 3 | prstcbas | |
5 | eqidd | |
|
6 | 1 2 5 | prstcleval | |
7 | fvex | Could not format ( ProsetToCat ` K ) e. _V : No typesetting found for |- ( ProsetToCat ` K ) e. _V with typecode |- | |
8 | 1 7 | eqeltrdi | |
9 | 4 6 8 | isprsd | |
10 | 3 5 2 | isprsd | |
11 | 9 10 | bitr4d | |
12 | 2 11 | mpbird | |