Definition df-bj-sethom 35221

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

Remark: one may define Set⟶ = (𝑥 ∈ dom Struct , 𝑦 ∈ dom Struct ↦ {𝑓 ∣ 𝑓:(Base‘𝑥)⟶(Base‘𝑦)}) so that for morphisms between other structures, one could write ... = {𝑓 ∈ (𝑥 Set⟶ 𝑦) ∣ ...}.

(Contributed by BJ, 11-Apr-2020.)

Assertion

Ref	Expression
df-bj-sethom	⊢ Set⟶ = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑥⟶𝑦})

Distinct variable group:   𝑥,𝑓,𝑦

Detailed syntax breakdown of Definition df-bj-sethom

Step	Hyp	Ref	Expression
1		csethom 35220	. 2 class Set⟶
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cvv 3422	. . 3 class V
5	2	cv 1538	. . . . 5 class 𝑥
6	3	cv 1538	. . . . 5 class 𝑦
7		vf	. . . . . 6 setvar 𝑓
8	7	cv 1538	. . . . 5 class 𝑓
9	5, 6, 8	wf 6414	. . . 4 wff 𝑓:𝑥⟶𝑦
10	9, 7	cab 2715	. . 3 class {𝑓 ∣ 𝑓:𝑥⟶𝑦}
11	2, 3, 4, 4, 10	cmpo 7257	. 2 class (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑥⟶𝑦})
12	1, 11	wceq 1539	1 wff Set⟶ = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑥⟶𝑦})

This definition is referenced by: (None)