Theorem ressle

Description: le is unaffected by restriction. (Contributed by Mario Carneiro, 3-Nov-2015)

	Ref	Expression
Hypotheses	ressle.1	$$⊢W=K{\upharpoonright }_{𝑠}A$$
	ressle.2	$$⊢\underset{\dot{}}{\le }={\le }_K$$
Assertion	ressle	$$⊢A\in V\to \underset{\dot{}}{\le }={\le }_W$$

Proof

Step	Hyp	Ref	Expression
1		ressle.1	$$⊢W=K{\upharpoonright }_{𝑠}A$$
2		ressle.2	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		pleid	$$⊢\mathrm{le}=\mathrm{Slot}{\le }_{\mathrm{ndx}}$$
4		plendxnbasendx	$$⊢{\le }_{\mathrm{ndx}}\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
5	1 2 3 4	resseqnbas	$$⊢A\in V\to \underset{\dot{}}{\le }={\le }_W$$