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 
|- ( ph -> C = ( ProsetToCat ` K ) )
prstcnid.k 
|- ( ph -> K e. Proset )
Assertion prstcval 
|- ( ph -> C = ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) )

Proof

Step Hyp Ref Expression
1 prstcnid.c 
 |-  ( ph -> C = ( ProsetToCat ` K ) )
2 prstcnid.k 
 |-  ( ph -> K e. Proset )
3 id 
 |-  ( k = K -> k = K )
4 fveq2 
 |-  ( k = K -> ( le ` k ) = ( le ` K ) )
5 4 xpeq1d 
 |-  ( k = K -> ( ( le ` k ) X. { 1o } ) = ( ( le ` K ) X. { 1o } ) )
6 5 opeq2d 
 |-  ( k = K -> <. ( Hom ` ndx ) , ( ( le ` k ) X. { 1o } ) >. = <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. )
7 3 6 oveq12d 
 |-  ( k = K -> ( k sSet <. ( Hom ` ndx ) , ( ( le ` k ) X. { 1o } ) >. ) = ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) )
8 7 oveq1d 
 |-  ( k = K -> ( ( k sSet <. ( Hom ` ndx ) , ( ( le ` k ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) = ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) )
9 df-prstc 
 |-  ProsetToCat = ( k e. Proset |-> ( ( k sSet <. ( Hom ` ndx ) , ( ( le ` k ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) )
10 ovex 
 |-  ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) e. _V
11 8 9 10 fvmpt 
 |-  ( K e. Proset -> ( ProsetToCat ` K ) = ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) )
12 2 11 syl 
 |-  ( ph -> ( ProsetToCat ` K ) = ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) )
13 1 12 eqtrd 
 |-  ( ph -> C = ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) )