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

Metamath Proof Explorer

Theorem estrchomfeqhom

Description: The functionalized Hom-set operation equals the Hom-set operation in the category of extensible structures (in a universe). (Contributed by AV, 8-Mar-2020)

Ref Expression
Hypotheses estrchomfn.c 
|- C = ( ExtStrCat ` U )
estrchomfn.u 
|- ( ph -> U e. V )
estrchomfn.h 
|- H = ( Hom ` C )
Assertion estrchomfeqhom 
|- ( ph -> ( Homf ` C ) = H )

Proof

Step Hyp Ref Expression
1 estrchomfn.c 
 |-  C = ( ExtStrCat ` U )
2 estrchomfn.u 
 |-  ( ph -> U e. V )
3 estrchomfn.h 
 |-  H = ( Hom ` C )
4 1 2 3 estrchomfn 
 |-  ( ph -> H Fn ( U X. U ) )
5 1 2 estrcbas 
 |-  ( ph -> U = ( Base ` C ) )
6 5 eqcomd 
 |-  ( ph -> ( Base ` C ) = U )
7 6 sqxpeqd 
 |-  ( ph -> ( ( Base ` C ) X. ( Base ` C ) ) = ( U X. U ) )
8 7 fneq2d 
 |-  ( ph -> ( H Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> H Fn ( U X. U ) ) )
9 4 8 mpbird 
 |-  ( ph -> H Fn ( ( Base ` C ) X. ( Base ` C ) ) )
10 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
11 eqid 
 |-  ( Base ` C ) = ( Base ` C )
12 10 11 3 fnhomeqhomf 
 |-  ( H Fn ( ( Base ` C ) X. ( Base ` C ) ) -> ( Homf ` C ) = H )
13 9 12 syl 
 |-  ( ph -> ( Homf ` C ) = H )