Metamath Proof Explorer


Theorem elsetchom

Description: A morphism of sets is a function. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses setcbas.c
|- C = ( SetCat ` U )
setcbas.u
|- ( ph -> U e. V )
setchomfval.h
|- H = ( Hom ` C )
setchom.x
|- ( ph -> X e. U )
setchom.y
|- ( ph -> Y e. U )
Assertion elsetchom
|- ( ph -> ( F e. ( X H Y ) <-> F : X --> Y ) )

Proof

Step Hyp Ref Expression
1 setcbas.c
 |-  C = ( SetCat ` U )
2 setcbas.u
 |-  ( ph -> U e. V )
3 setchomfval.h
 |-  H = ( Hom ` C )
4 setchom.x
 |-  ( ph -> X e. U )
5 setchom.y
 |-  ( ph -> Y e. U )
6 1 2 3 4 5 setchom
 |-  ( ph -> ( X H Y ) = ( Y ^m X ) )
7 6 eleq2d
 |-  ( ph -> ( F e. ( X H Y ) <-> F e. ( Y ^m X ) ) )
8 5 4 elmapd
 |-  ( ph -> ( F e. ( Y ^m X ) <-> F : X --> Y ) )
9 7 8 bitrd
 |-  ( ph -> ( F e. ( X H Y ) <-> F : X --> Y ) )