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

Definition df-ress 11749
 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 11742 . 2 class s
2 vw . . 3 setvar 𝑤
3 vx . . 3 setvar 𝑥
4 cvv 2641 . . 3 class V
52cv 1298 . . . . . 6 class 𝑤
6 cbs 11741 . . . . . 6 class Base
75, 6cfv 5059 . . . . 5 class (Base‘𝑤)
83cv 1298 . . . . 5 class 𝑥
97, 8wss 3021 . . . 4 wff (Base‘𝑤) ⊆ 𝑥
10 cnx 11738 . . . . . . 7 class ndx
1110, 6cfv 5059 . . . . . 6 class (Base‘ndx)
128, 7cin 3020 . . . . . 6 class (𝑥 ∩ (Base‘𝑤))
1311, 12cop 3477 . . . . 5 class ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩
14 csts 11739 . . . . 5 class sSet
155, 13, 14co 5706 . . . 4 class (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)
169, 5, 15cif 3421 . . 3 class if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩))
172, 3, 4, 4, 16cmpo 5708 . 2 class (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))
181, 17wceq 1299 1 wff s = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))
 Colors of variables: wff set class This definition is referenced by:  reldmress  11799  ressid2  11800  ressval2  11801
 Copyright terms: Public domain W3C validator