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 ( see prstchom2ALT ). However, this should not be assumed as it is definition-dependent. Therefore, the two hypotheses are added for explicitness. (Contributed by Zhi Wang, 21-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 | prstchom2 | |- ( ph -> ( X .<_ Y <-> E! f f e. ( 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 4 5 6 | prstchom | |- ( ph -> ( X .<_ Y <-> ( X H Y ) =/= (/) ) ) |
| 8 | 1 2 | prstcthin | |- ( ph -> C e. ThinCat ) |
| 9 | eqidd | |- ( ph -> ( Base ` C ) = ( Base ` C ) ) |
|
| 10 | 8 5 6 9 4 | thincn0eu | |- ( ph -> ( ( X H Y ) =/= (/) <-> E! f f e. ( X H Y ) ) ) |
| 11 | 7 10 | bitrd | |- ( ph -> ( X .<_ Y <-> E! f f e. ( X H Y ) ) ) |