ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ress GIF version

Definition df-ress 11981
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.)

Assertion
Ref Expression
df-ress s = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))
Distinct variable group:   𝑥,𝑤

Detailed syntax breakdown of Definition df-ress
StepHypRef Expression
1 cress 11974 . 2 class s
2 vw . . 3 setvar 𝑤
3 vx . . 3 setvar 𝑥
4 cvv 2686 . . 3 class V
52cv 1330 . . . . . 6 class 𝑤
6 cbs 11973 . . . . . 6 class Base
75, 6cfv 5123 . . . . 5 class (Base‘𝑤)
83cv 1330 . . . . 5 class 𝑥
97, 8wss 3071 . . . 4 wff (Base‘𝑤) ⊆ 𝑥
10 cnx 11970 . . . . . . 7 class ndx
1110, 6cfv 5123 . . . . . 6 class (Base‘ndx)
128, 7cin 3070 . . . . . 6 class (𝑥 ∩ (Base‘𝑤))
1311, 12cop 3530 . . . . 5 class ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩
14 csts 11971 . . . . 5 class sSet
155, 13, 14co 5774 . . . 4 class (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)
169, 5, 15cif 3474 . . 3 class if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩))
172, 3, 4, 4, 16cmpo 5776 . 2 class (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))
181, 17wceq 1331 1 wff s = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))
Colors of variables: wff set class
This definition is referenced by:  reldmress  12031  ressid2  12032  ressval2  12033
  Copyright terms: Public domain W3C validator