Definition df-ress 12402

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

Step	Hyp	Ref	Expression
1		cress 12395	. 2 class ↾s
2		vw	. . 3 setvar 𝑤
3		vx	. . 3 setvar 𝑥
4		cvv 2726	. . 3 class V
5	2	cv 1342	. . . . . 6 class 𝑤
6		cbs 12394	. . . . . 6 class Base
7	5, 6	cfv 5188	. . . . 5 class (Base‘𝑤)
8	3	cv 1342	. . . . 5 class 𝑥
9	7, 8	wss 3116	. . . 4 wff (Base‘𝑤) ⊆ 𝑥
10		cnx 12391	. . . . . . 7 class ndx
11	10, 6	cfv 5188	. . . . . 6 class (Base‘ndx)
12	8, 7	cin 3115	. . . . . 6 class (𝑥 ∩ (Base‘𝑤))
13	11, 12	cop 3579	. . . . 5 class ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩
14		csts 12392	. . . . 5 class sSet
15	5, 13, 14	co 5842	. . . 4 class (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)
16	9, 5, 15	cif 3520	. . 3 class if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩))
17	2, 3, 4, 4, 16	cmpo 5844	. 2 class (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))
18	1, 17	wceq 1343	1 wff ↾s = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))

This definition is referenced by:  reldmress  12453  ressid2  12454  ressval2  12455