Metamath Proof Explorer


Theorem prstcval

Description: Lemma for prstcnidlem and prstcthin . (Contributed by Zhi Wang, 20-Sep-2024) (New usage is discouraged.)

Ref Expression
Hypotheses prstcnid.c No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
prstcnid.k φKProset
Assertion prstcval φC=KsSetHomndxK×1𝑜sSetcompndx

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 id k=Kk=K
4 fveq2 k=Kk=K
5 4 xpeq1d k=Kk×1𝑜=K×1𝑜
6 5 opeq2d k=KHomndxk×1𝑜=HomndxK×1𝑜
7 3 6 oveq12d k=KksSetHomndxk×1𝑜=KsSetHomndxK×1𝑜
8 7 oveq1d k=KksSetHomndxk×1𝑜sSetcompndx=KsSetHomndxK×1𝑜sSetcompndx
9 df-prstc Could not format ProsetToCat = ( k e. Proset |-> ( ( k sSet <. ( Hom ` ndx ) , ( ( le ` k ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) : No typesetting found for |- ProsetToCat = ( k e. Proset |-> ( ( k sSet <. ( Hom ` ndx ) , ( ( le ` k ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) with typecode |-
10 ovex KsSetHomndxK×1𝑜sSetcompndxV
11 8 9 10 fvmpt Could not format ( K e. Proset -> ( ProsetToCat ` K ) = ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) : No typesetting found for |- ( K e. Proset -> ( ProsetToCat ` K ) = ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) with typecode |-
12 2 11 syl Could not format ( ph -> ( ProsetToCat ` K ) = ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) : No typesetting found for |- ( ph -> ( ProsetToCat ` K ) = ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) with typecode |-
13 1 12 eqtrd φC=KsSetHomndxK×1𝑜sSetcompndx