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

Metamath Proof Explorer

Theorem estrchomfn

Description: The Hom-set operation in the category of extensible structures (in a universe) is a function. (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 estrchomfn 
|- ( ph -> H Fn ( U X. U ) )

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 eqid 
 |-  ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) )
5 ovex 
 |-  ( ( Base ` y ) ^m ( Base ` x ) ) e. _V
6 4 5 fnmpoi 
 |-  ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) Fn ( U X. U )
7 1 2 3 estrchomfval 
 |-  ( ph -> H = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
8 7 fneq1d 
 |-  ( ph -> ( H Fn ( U X. U ) <-> ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) Fn ( U X. U ) ) )
9 6 8 mpbiri 
 |-  ( ph -> H Fn ( U X. U ) )