Theorem ressco

Description: comp is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017)

	Ref	Expression
Hypotheses	resshom.1	$$⊢D=C{\upharpoonright }_{𝑠}A$$
	ressco.2	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
Assertion	ressco	$$⊢A\in V\to \underset{\dot{}}{·}=\mathrm{comp}\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		resshom.1	$$⊢D=C{\upharpoonright }_{𝑠}A$$
2		ressco.2	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
3		ccoid	$$⊢\mathrm{comp}=\mathrm{Slot}\mathrm{comp}\left(\mathrm{ndx}\right)$$
4		slotsbhcdif	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\wedge \mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\right)$$
5		simp2	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\wedge \mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\right)\to {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
6	5	necomd	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\wedge \mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\right)\to \mathrm{comp}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
7	4 6	ax-mp	$$⊢\mathrm{comp}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
8	1 2 3 7	resseqnbas	$$⊢A\in V\to \underset{\dot{}}{·}=\mathrm{comp}\left(D\right)$$