Definition df-ress 17370

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 (like Ring), defining a function using the base set and applying that (like TopGrp), or explicitly truncating the slot before use (like MetSp).

(Credit for this operator goes to Mario Carneiro.)

See ressbas 17375 for the altered base set, and resseqnbas 17381 (subrg0 20792, ressplusg 17423, subrg1 20795, ressmulr 17439) for the (un)altered other operations. (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 17369	. 2 class ↾s
2		vw	. . 3 setvar 𝑤
3		vx	. . 3 setvar 𝑥
4		cvv 3450	. . 3 class V
5	2	cv 1569	. . . . . 6 class 𝑤
6		cbs 17348	. . . . . 6 class Base
7	5, 6	cfv 6527	. . . . 5 class (Base‘𝑤)
8	3	cv 1569	. . . . 5 class 𝑥
9	7, 8	wss 3898	. . . 4 wff (Base‘𝑤) ⊆ 𝑥
10		cnx 17332	. . . . . . 7 class ndx
11	10, 6	cfv 6527	. . . . . 6 class (Base‘ndx)
12	8, 7	cin 3897	. . . . . 6 class (𝑥 ∩ (Base‘𝑤))
13	11, 12	cop 4589	. . . . 5 class ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩
14		csts 17302	. . . . 5 class sSet
15	5, 13, 14	co 7408	. . . 4 class (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)
16	9, 5, 15	cif 4481	. . 3 class if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩))
17	2, 3, 4, 4, 16	cmpo 7410	. 2 class (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))
18	1, 17	wceq 1570	1 wff ↾s = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))

This definition is used by:  reldmress  17371  ressval  17372