Definition df-ress 12417

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 = ( w e. _V , x e. _V |-> if ( ( Base ` w ) C_ x , w , ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) ) )

Distinct variable group:   x, w

Detailed syntax breakdown of Definition df-ress

Step	Hyp	Ref	Expression
1		cress 12410	. 2 class ↾s
2		vw	. . 3 setvar w
3		vx	. . 3 setvar x
4		cvv 2730	. . 3 class _V
5	2	cv 1347	. . . . . 6 class w
6		cbs 12409	. . . . . 6 class Base
7	5, 6	cfv 5196	. . . . 5 class ( Base ` w )
8	3	cv 1347	. . . . 5 class x
9	7, 8	wss 3121	. . . 4 wff ( Base ` w ) C_ x
10		cnx 12406	. . . . . . 7 class ndx
11	10, 6	cfv 5196	. . . . . 6 class ( Base ` ndx )
12	8, 7	cin 3120	. . . . . 6 class ( x i^i ( Base ` w ) )
13	11, 12	cop 3584	. . . . 5 class <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >.
14		csts 12407	. . . . 5 class sSet
15	5, 13, 14	co 5851	. . . 4 class ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. )
16	9, 5, 15	cif 3525	. . 3 class if ( ( Base ` w ) C_ x , w , ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
17	2, 3, 4, 4, 16	cmpo 5853	. 2 class ( w e. _V , x e. _V |-> if ( ( Base ` w ) C_ x , w , ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) ) )
18	1, 17	wceq 1348	1 wff ↾s = ( w e. _V , x e. _V |-> if ( ( Base ` w ) C_ x , w , ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) ) )

This definition is referenced by:  reldmress  12469  ressid2  12470  ressval2  12471