Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-ress | GIF version |
Description: Define a multifunction
restriction operator for extensible structures,
which can be used to turn statements about rings into statements about
subrings, modules into submodules, etc. This definition knows nothing
about individual structures and merely truncates the Base set while
leaving operators alone; individual kinds of structures will need to
handle this behavior, by ignoring operators' values outside the range,
defining a function using the base set and applying that, or explicitly
truncating the slot before use.
(Credit for this operator goes to Mario Carneiro.) (Contributed by Stefan O'Rear, 29-Nov-2014.) |
Ref | Expression |
---|---|
df-ress | ⊢ ↾s = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet 〈(Base‘ndx), (𝑥 ∩ (Base‘𝑤))〉))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cress 11960 | . 2 class ↾s | |
2 | vw | . . 3 setvar 𝑤 | |
3 | vx | . . 3 setvar 𝑥 | |
4 | cvv 2686 | . . 3 class V | |
5 | 2 | cv 1330 | . . . . . 6 class 𝑤 |
6 | cbs 11959 | . . . . . 6 class Base | |
7 | 5, 6 | cfv 5123 | . . . . 5 class (Base‘𝑤) |
8 | 3 | cv 1330 | . . . . 5 class 𝑥 |
9 | 7, 8 | wss 3071 | . . . 4 wff (Base‘𝑤) ⊆ 𝑥 |
10 | cnx 11956 | . . . . . . 7 class ndx | |
11 | 10, 6 | cfv 5123 | . . . . . 6 class (Base‘ndx) |
12 | 8, 7 | cin 3070 | . . . . . 6 class (𝑥 ∩ (Base‘𝑤)) |
13 | 11, 12 | cop 3530 | . . . . 5 class 〈(Base‘ndx), (𝑥 ∩ (Base‘𝑤))〉 |
14 | csts 11957 | . . . . 5 class sSet | |
15 | 5, 13, 14 | co 5774 | . . . 4 class (𝑤 sSet 〈(Base‘ndx), (𝑥 ∩ (Base‘𝑤))〉) |
16 | 9, 5, 15 | cif 3474 | . . 3 class if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet 〈(Base‘ndx), (𝑥 ∩ (Base‘𝑤))〉)) |
17 | 2, 3, 4, 4, 16 | cmpo 5776 | . 2 class (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet 〈(Base‘ndx), (𝑥 ∩ (Base‘𝑤))〉))) |
18 | 1, 17 | wceq 1331 | 1 wff ↾s = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet 〈(Base‘ndx), (𝑥 ∩ (Base‘𝑤))〉))) |
Colors of variables: wff set class |
This definition is referenced by: reldmress 12017 ressid2 12018 ressval2 12019 |
Copyright terms: Public domain | W3C validator |