Metamath Proof Explorer


Theorem prstchom2

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 No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
prstcnid.k φKProset
prstchom.l φ˙=C
prstchom.e φH=HomC
prstchom.x φXBaseC
prstchom.y φYBaseC
Assertion prstchom2 φX˙Y∃!ffXHY

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 prstchom.l φ˙=C
4 prstchom.e φH=HomC
5 prstchom.x φXBaseC
6 prstchom.y φYBaseC
7 1 2 3 4 5 6 prstchom φX˙YXHY
8 1 2 prstcthin Could not format ( ph -> C e. ThinCat ) : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
9 eqidd φBaseC=BaseC
10 8 5 6 9 4 thincn0eu φXHY∃!ffXHY
11 7 10 bitrd φX˙Y∃!ffXHY