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 𝐶 = ( SetCat ‘ 𝑈 )
setcbas.u ( 𝜑𝑈𝑉 )
setchomfval.h 𝐻 = ( Hom ‘ 𝐶 )
setchom.x ( 𝜑𝑋𝑈 )
setchom.y ( 𝜑𝑌𝑈 )
Assertion elsetchom ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ↔ 𝐹 : 𝑋𝑌 ) )

Proof

Step Hyp Ref Expression
1 setcbas.c 𝐶 = ( SetCat ‘ 𝑈 )
2 setcbas.u ( 𝜑𝑈𝑉 )
3 setchomfval.h 𝐻 = ( Hom ‘ 𝐶 )
4 setchom.x ( 𝜑𝑋𝑈 )
5 setchom.y ( 𝜑𝑌𝑈 )
6 1 2 3 4 5 setchom ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝑌m 𝑋 ) )
7 6 eleq2d ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ↔ 𝐹 ∈ ( 𝑌m 𝑋 ) ) )
8 5 4 elmapd ( 𝜑 → ( 𝐹 ∈ ( 𝑌m 𝑋 ) ↔ 𝐹 : 𝑋𝑌 ) )
9 7 8 bitrd ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ↔ 𝐹 : 𝑋𝑌 ) )