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		df-ple	$$⊢\mathrm{le}=\mathrm{Slot}10$$
4		10nn	$$⊢10\in \mathbb{N}$$
5		1lt10	$$⊢1<10$$
6	1 2 3 4 5	resslem	$$⊢A\in V\to \underset{\dot{}}{\le }={\le }_W$$