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 11887 | . 2 class ↾s | |
2 | vw | . . 3 setvar 𝑤 | |
3 | vx | . . 3 setvar 𝑥 | |
4 | cvv 2660 | . . 3 class V | |
5 | 2 | cv 1315 | . . . . . 6 class 𝑤 |
6 | cbs 11886 | . . . . . 6 class Base | |
7 | 5, 6 | cfv 5093 | . . . . 5 class (Base‘𝑤) |
8 | 3 | cv 1315 | . . . . 5 class 𝑥 |
9 | 7, 8 | wss 3041 | . . . 4 wff (Base‘𝑤) ⊆ 𝑥 |
10 | cnx 11883 | . . . . . . 7 class ndx | |
11 | 10, 6 | cfv 5093 | . . . . . 6 class (Base‘ndx) |
12 | 8, 7 | cin 3040 | . . . . . 6 class (𝑥 ∩ (Base‘𝑤)) |
13 | 11, 12 | cop 3500 | . . . . 5 class 〈(Base‘ndx), (𝑥 ∩ (Base‘𝑤))〉 |
14 | csts 11884 | . . . . 5 class sSet | |
15 | 5, 13, 14 | co 5742 | . . . 4 class (𝑤 sSet 〈(Base‘ndx), (𝑥 ∩ (Base‘𝑤))〉) |
16 | 9, 5, 15 | cif 3444 | . . 3 class if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet 〈(Base‘ndx), (𝑥 ∩ (Base‘𝑤))〉)) |
17 | 2, 3, 4, 4, 16 | cmpo 5744 | . 2 class (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet 〈(Base‘ndx), (𝑥 ∩ (Base‘𝑤))〉))) |
18 | 1, 17 | wceq 1316 | 1 wff ↾s = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet 〈(Base‘ndx), (𝑥 ∩ (Base‘𝑤))〉))) |
Colors of variables: wff set class |
This definition is referenced by: reldmress 11944 ressid2 11945 ressval2 11946 |
Copyright terms: Public domain | W3C validator |