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⟶ = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑓 ∣ 𝑓 : 𝑥 ⟶ 𝑦 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csethom	⊢ Set⟶
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vy	⊢ 𝑦
4		vf	⊢ 𝑓
5	4	cv	⊢ 𝑓
6	1	cv	⊢ 𝑥
7	3	cv	⊢ 𝑦
8	6 7 5	wf	⊢ 𝑓 : 𝑥 ⟶ 𝑦
9	8 4	cab	⊢ { 𝑓 ∣ 𝑓 : 𝑥 ⟶ 𝑦 }
10	1 3 2 2 9	cmpo	⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑓 ∣ 𝑓 : 𝑥 ⟶ 𝑦 } )
11	0 10	wceq	⊢ Set⟶ = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑓 ∣ 𝑓 : 𝑥 ⟶ 𝑦 } )