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	$$⊢\underset{Set}{⟶}=\left(x\in \mathrm{V},y\in \mathrm{V}⟼\left\{f|f:x⟶y\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csethom	$$class\underset{Set}{⟶}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vy	$$setvary$$
4		vf	$$setvarf$$
5	4	cv	$$setvarf$$
6	1	cv	$$setvarx$$
7	3	cv	$$setvary$$
8	6 7 5	wf	$$wfff:x⟶y$$
9	8 4	cab	$$class\left\{f|f:x⟶y\right\}$$
10	1 3 2 2 9	cmpo	$$class\left(x\in \mathrm{V},y\in \mathrm{V}⟼\left\{f|f:x⟶y\right\}\right)$$
11	0 10	wceq	$$wff\underset{Set}{⟶}=\left(x\in \mathrm{V},y\in \mathrm{V}⟼\left\{f|f:x⟶y\right\}\right)$$