Definition df-bj-sethom

Description: Define the set of functions (morphisms of sets) between two sets. Same as df-map with arguments swapped. TODO: prove the same staple lemmas as for ^m .

Remark: one may define -Set-> = ( x e. dom Struct , y e. dom Struct |-> { f | f : ( Basex ) --> ( Basey ) } ) so that for morphisms between other structures, one could write ... = { f e. ( x -Set-> y ) | ... } .

(Contributed by BJ, 11-Apr-2020)

	Ref	Expression
Assertion	df-bj-sethom	|- -Set-> = ( x e. _V , y e. _V |-> { f | f : x --> y } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csethom	|- -Set->
1		vx	|- x
2		cvv	|- _V
3		vy	|- y
4		vf	|- f
5	4	cv	|- f
6	1	cv	|- x
7	3	cv	|- y
8	6 7 5	wf	|- f : x --> y
9	8 4	cab	|- { f | f : x --> y }
10	1 3 2 2 9	cmpo	|- ( x e. _V , y e. _V |-> { f | f : x --> y } )
11	0 10	wceq	|- -Set-> = ( x e. _V , y e. _V |-> { f | f : x --> y } )