Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-assintop | Structured version Visualization version GIF version |
Description: Function mapping a set to the class of all associative (closed internal binary) operations for this set, see definition 5 in [BourbakiAlg1] p. 4, where it is called "an associative law of composition". (Contributed by AV, 20-Jan-2020.) |
Ref | Expression |
---|---|
df-assintop | ⊢ assIntOp = (𝑚 ∈ V ↦ {𝑜 ∈ ( clIntOp ‘𝑚) ∣ 𝑜 assLaw 𝑚}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cassintop 45370 | . 2 class assIntOp | |
2 | vm | . . 3 setvar 𝑚 | |
3 | cvv 3429 | . . 3 class V | |
4 | vo | . . . . . 6 setvar 𝑜 | |
5 | 4 | cv 1538 | . . . . 5 class 𝑜 |
6 | 2 | cv 1538 | . . . . 5 class 𝑚 |
7 | casslaw 45356 | . . . . 5 class assLaw | |
8 | 5, 6, 7 | wbr 5073 | . . . 4 wff 𝑜 assLaw 𝑚 |
9 | cclintop 45369 | . . . . 5 class clIntOp | |
10 | 6, 9 | cfv 6426 | . . . 4 class ( clIntOp ‘𝑚) |
11 | 8, 4, 10 | crab 3068 | . . 3 class {𝑜 ∈ ( clIntOp ‘𝑚) ∣ 𝑜 assLaw 𝑚} |
12 | 2, 3, 11 | cmpt 5156 | . 2 class (𝑚 ∈ V ↦ {𝑜 ∈ ( clIntOp ‘𝑚) ∣ 𝑜 assLaw 𝑚}) |
13 | 1, 12 | wceq 1539 | 1 wff assIntOp = (𝑚 ∈ V ↦ {𝑜 ∈ ( clIntOp ‘𝑚) ∣ 𝑜 assLaw 𝑚}) |
Colors of variables: wff setvar class |
This definition is referenced by: assintopval 45377 |
Copyright terms: Public domain | W3C validator |