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 | ⊢ 𝑂 = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , 𝑆 ⟩ ) | |
| setsplusg.e | ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx ) | ||
| setsplusg.i | ⊢ ( 𝐸 ‘ ndx ) ≠ ( +g ‘ ndx ) | ||
| Assertion | setsplusg | ⊢ ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑂 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | setsplusg.o | ⊢ 𝑂 = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , 𝑆 ⟩ ) | |
| 2 | setsplusg.e | ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx ) | |
| 3 | setsplusg.i | ⊢ ( 𝐸 ‘ ndx ) ≠ ( +g ‘ ndx ) | |
| 4 | 2 3 | setsnid | ⊢ ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , 𝑆 ⟩ ) ) |
| 5 | 1 | fveq2i | ⊢ ( 𝐸 ‘ 𝑂 ) = ( 𝐸 ‘ ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , 𝑆 ⟩ ) ) |
| 6 | 4 5 | eqtr4i | ⊢ ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑂 ) |