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

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	$⊢ φ \to U \in V$
	setchomfval.h	$⊢ H = Hom (C)$
	setchom.x	$⊢ φ \to X \in U$
	setchom.y	$⊢ φ \to Y \in U$
Assertion	elsetchom	$⊢ φ \to (F \in (X H Y) \leftrightarrow F : X ⟶ Y)$

Step	Hyp	Ref	Expression
1		setcbas.c	$⊢ C = SetCat (U)$
2		setcbas.u	$⊢ φ \to U \in V$
3		setchomfval.h	$⊢ H = Hom (C)$
4		setchom.x	$⊢ φ \to X \in U$
5		setchom.y	$⊢ φ \to Y \in U$
6	1 2 3 4 5	setchom	$⊢ φ \to X H Y = Y^{X}$
7	6	eleq2d	$⊢ φ \to (F \in (X H Y) \leftrightarrow F \in (Y^{X}))$
8	5 4	elmapd	$⊢ φ \to (F \in (Y^{X}) \leftrightarrow F : X ⟶ Y)$
9	7 8	bitrd	$⊢ φ \to (F \in (X H Y) \leftrightarrow F : X ⟶ Y)$