Description: The other components of an extensible structure remain unchanged if the +g component is set/substituted. (Contributed by Stefan O'Rear, 26-Aug-2015) Generalisation of the former oppglem and mgplem. (Revised by AV, 18-Oct-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | setsplusg.o | |- O = ( R sSet <. ( +g ` ndx ) , S >. ) |
|
| setsplusg.e | |- E = Slot ( E ` ndx ) |
||
| setsplusg.i | |- ( E ` ndx ) =/= ( +g ` ndx ) |
||
| Assertion | setsplusg | |- ( E ` R ) = ( E ` O ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | setsplusg.o | |- O = ( R sSet <. ( +g ` ndx ) , S >. ) |
|
| 2 | setsplusg.e | |- E = Slot ( E ` ndx ) |
|
| 3 | setsplusg.i | |- ( E ` ndx ) =/= ( +g ` ndx ) |
|
| 4 | 2 3 | setsnid | |- ( E ` R ) = ( E ` ( R sSet <. ( +g ` ndx ) , S >. ) ) |
| 5 | 1 | fveq2i | |- ( E ` O ) = ( E ` ( R sSet <. ( +g ` ndx ) , S >. ) ) |
| 6 | 4 5 | eqtr4i | |- ( E ` R ) = ( E ` O ) |