Theorem eqfunressuc

Description: Law for equality of restriction to successors. This is primarily useful when X is an ordinal, but it does not require that. (Contributed by Scott Fenton, 6-Dec-2021)

	Ref	Expression
Assertion	eqfunressuc	$$⊢\left(\left(\mathrm{Fun}F\wedge \mathrm{Fun}G\right)\wedge {F\upharpoonright }_X={G\upharpoonright }_X\wedge \left(X\in \mathrm{dom}F\wedge X\in \mathrm{dom}G\wedge F\left(X\right)=G\left(X\right)\right)\right)\to {F\upharpoonright }_{\mathrm{suc}X}={G\upharpoonright }_{\mathrm{suc}X}$$

Proof

Step	Hyp	Ref	Expression
1		eqfunresadj	$$⊢\left(\left(\mathrm{Fun}F\wedge \mathrm{Fun}G\right)\wedge {F\upharpoonright }_X={G\upharpoonright }_X\wedge \left(X\in \mathrm{dom}F\wedge X\in \mathrm{dom}G\wedge F\left(X\right)=G\left(X\right)\right)\right)\to {F\upharpoonright }_{\left(X\cup \left\{X\right\}\right)}={G\upharpoonright }_{\left(X\cup \left\{X\right\}\right)}$$
2		df-suc	$$⊢\mathrm{suc}X=X\cup \left\{X\right\}$$
3	2	reseq2i	$$⊢{F\upharpoonright }_{\mathrm{suc}X}={F\upharpoonright }_{\left(X\cup \left\{X\right\}\right)}$$
4	2	reseq2i	$$⊢{G\upharpoonright }_{\mathrm{suc}X}={G\upharpoonright }_{\left(X\cup \left\{X\right\}\right)}$$
5	1 3 4	3eqtr4g	$$⊢\left(\left(\mathrm{Fun}F\wedge \mathrm{Fun}G\right)\wedge {F\upharpoonright }_X={G\upharpoonright }_X\wedge \left(X\in \mathrm{dom}F\wedge X\in \mathrm{dom}G\wedge F\left(X\right)=G\left(X\right)\right)\right)\to {F\upharpoonright }_{\mathrm{suc}X}={G\upharpoonright }_{\mathrm{suc}X}$$