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

Definition df-ress 11894
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 11887 . 2 class s
2 vw . . 3 setvar 𝑤
3 vx . . 3 setvar 𝑥
4 cvv 2660 . . 3 class V
52cv 1315 . . . . . 6 class 𝑤
6 cbs 11886 . . . . . 6 class Base
75, 6cfv 5093 . . . . 5 class (Base‘𝑤)
83cv 1315 . . . . 5 class 𝑥
97, 8wss 3041 . . . 4 wff (Base‘𝑤) ⊆ 𝑥
10 cnx 11883 . . . . . . 7 class ndx
1110, 6cfv 5093 . . . . . 6 class (Base‘ndx)
128, 7cin 3040 . . . . . 6 class (𝑥 ∩ (Base‘𝑤))
1311, 12cop 3500 . . . . 5 class ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩
14 csts 11884 . . . . 5 class sSet
155, 13, 14co 5742 . . . 4 class (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)
169, 5, 15cif 3444 . . 3 class if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩))
172, 3, 4, 4, 16cmpo 5744 . 2 class (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))
181, 17wceq 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