Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-sethom Structured version   Visualization version   GIF version

Definition df-bj-sethom 34533
Description: Define the set of functions (morphisms of sets) between two sets. Same as df-map 8395 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
StepHypRef Expression
1 csethom 34532 . 2 class Set
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cvv 3444 . . 3 class V
52cv 1537 . . . . 5 class 𝑥
63cv 1537 . . . . 5 class 𝑦
7 vf . . . . . 6 setvar 𝑓
87cv 1537 . . . . 5 class 𝑓
95, 6, 8wf 6324 . . . 4 wff 𝑓:𝑥𝑦
109, 7cab 2779 . . 3 class {𝑓𝑓:𝑥𝑦}
112, 3, 4, 4, 10cmpo 7141 . 2 class (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓𝑓:𝑥𝑦})
121, 11wceq 1538 1 wff Set⟶ = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓𝑓:𝑥𝑦})
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator