Description: Hom-sets of the constructed category are dependent on the preorder.
Note that prstchom.x and prstchom.y are redundant here due to our definition of ProsetToCat . However, this should not be assumed as it is definition-dependent. Therefore, the two hypotheses are added for explicitness. (Contributed by Zhi Wang, 20-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | prstcnid.c | |- ( ph -> C = ( ProsetToCat ` K ) ) |
|
| prstcnid.k | |- ( ph -> K e. Proset ) |
||
| prstchom.l | |- ( ph -> .<_ = ( le ` C ) ) |
||
| prstchom.e | |- ( ph -> H = ( Hom ` C ) ) |
||
| prstchom.x | |- ( ph -> X e. ( Base ` C ) ) |
||
| prstchom.y | |- ( ph -> Y e. ( Base ` C ) ) |
||
| Assertion | prstchom | |- ( ph -> ( X .<_ Y <-> ( X H Y ) =/= (/) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | prstcnid.c | |- ( ph -> C = ( ProsetToCat ` K ) ) |
|
| 2 | prstcnid.k | |- ( ph -> K e. Proset ) |
|
| 3 | prstchom.l | |- ( ph -> .<_ = ( le ` C ) ) |
|
| 4 | prstchom.e | |- ( ph -> H = ( Hom ` C ) ) |
|
| 5 | prstchom.x | |- ( ph -> X e. ( Base ` C ) ) |
|
| 6 | prstchom.y | |- ( ph -> Y e. ( Base ` C ) ) |
|
| 7 | 1 2 3 | prstchomval | |- ( ph -> ( .<_ X. { 1o } ) = ( Hom ` C ) ) |
| 8 | 4 7 | eqtr4d | |- ( ph -> H = ( .<_ X. { 1o } ) ) |
| 9 | 1oex | |- 1o e. _V |
|
| 10 | 9 | a1i | |- ( ph -> 1o e. _V ) |
| 11 | 1n0 | |- 1o =/= (/) |
|
| 12 | 11 | a1i | |- ( ph -> 1o =/= (/) ) |
| 13 | 8 10 12 | fvconstrn0 | |- ( ph -> ( X .<_ Y <-> ( X H Y ) =/= (/) ) ) |