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

Metamath Proof Explorer

Theorem elrngchom

Description: A morphism of non-unital rings is a function. (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypotheses rngcbas.c 
|- C = ( RngCat ` U )
rngcbas.b 
|- B = ( Base ` C )
rngcbas.u 
|- ( ph -> U e. V )
rngchomfval.h 
|- H = ( Hom ` C )
rngchom.x 
|- ( ph -> X e. B )
rngchom.y 
|- ( ph -> Y e. B )
Assertion elrngchom 
|- ( ph -> ( F e. ( X H Y ) -> F : ( Base ` X ) --> ( Base ` Y ) ) )

Proof

Step Hyp Ref Expression
1 rngcbas.c 
 |-  C = ( RngCat ` U )
2 rngcbas.b 
 |-  B = ( Base ` C )
3 rngcbas.u 
 |-  ( ph -> U e. V )
4 rngchomfval.h 
 |-  H = ( Hom ` C )
5 rngchom.x 
 |-  ( ph -> X e. B )
6 rngchom.y 
 |-  ( ph -> Y e. B )
7 1 2 3 4 5 6 rngchom 
 |-  ( ph -> ( X H Y ) = ( X RngHom Y ) )
8 7 eleq2d 
 |-  ( ph -> ( F e. ( X H Y ) <-> F e. ( X RngHom Y ) ) )
9 eqid 
 |-  ( Base ` X ) = ( Base ` X )
10 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
11 9 10 rnghmf 
 |-  ( F e. ( X RngHom Y ) -> F : ( Base ` X ) --> ( Base ` Y ) )
12 8 11 biimtrdi 
 |-  ( ph -> ( F e. ( X H Y ) -> F : ( Base ` X ) --> ( Base ` Y ) ) )