Metamath Proof Explorer


Theorem prstcnid

Description: Components other than Hom and comp are unchanged. (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
prstcnid.e E=SlotEndx
prstcnid.no Endxcompndx
prstcnid.nh EndxHomndx
Assertion prstcnid φEK=EC

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 prstcnid.e E=SlotEndx
4 prstcnid.no Endxcompndx
5 prstcnid.nh EndxHomndx
6 3 5 setsnid EK=EKsSetHomndxK×1𝑜
7 1 2 3 4 prstcnidlem φEC=EKsSetHomndxK×1𝑜
8 6 7 eqtr4id φEK=EC