This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prstchomval

Description: Hom-sets of the constructed category which depend on an arbitrary definition. (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 )
prstchomval.l 
|- ( ph -> .<_ = ( le ` C ) )
Assertion prstchomval 
|- ( ph -> ( .<_ X. { 1o } ) = ( Hom ` C ) )

Proof

Step Hyp Ref Expression
1 prstcnid.c 
 |-  ( ph -> C = ( ProsetToCat ` K ) )
2 prstcnid.k 
 |-  ( ph -> K e. Proset )
3 prstchomval.l 
 |-  ( ph -> .<_ = ( le ` C ) )
4 homid 
 |-  Hom = Slot ( Hom ` ndx )
5 slotsbhcdif 
 |-  ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) )
6 5 simp3i 
 |-  ( Hom ` ndx ) =/= ( comp ` ndx )
7 1 2 4 6 prstcnidlem 
 |-  ( ph -> ( Hom ` C ) = ( Hom ` ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) ) )
8 fvex 
 |-  ( le ` K ) e. _V
9 snex 
 |-  { 1o } e. _V
10 8 9 xpex 
 |-  ( ( le ` K ) X. { 1o } ) e. _V
11 4 setsid 
 |-  ( ( K e. Proset /\ ( ( le ` K ) X. { 1o } ) e. _V ) -> ( ( le ` K ) X. { 1o } ) = ( Hom ` ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) ) )
12 2 10 11 sylancl 
 |-  ( ph -> ( ( le ` K ) X. { 1o } ) = ( Hom ` ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) ) )
13 eqidd 
 |-  ( ph -> ( le ` K ) = ( le ` K ) )
14 1 2 13 prstcleval 
 |-  ( ph -> ( le ` K ) = ( le ` C ) )
15 14 3 eqtr4d 
 |-  ( ph -> ( le ` K ) = .<_ )
16 15 xpeq1d 
 |-  ( ph -> ( ( le ` K ) X. { 1o } ) = ( .<_ X. { 1o } ) )
17 7 12 16 3eqtr2rd 
 |-  ( ph -> ( .<_ X. { 1o } ) = ( Hom ` C ) )