Metamath Proof Explorer
Description: le is unaffected by restriction. (Contributed by Mario Carneiro, 3-Nov-2015)
|
|
Ref |
Expression |
|
Hypotheses |
ressle.1 |
|
|
|
ressle.2 |
|
|
Assertion |
ressle |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
ressle.1 |
|
2 |
|
ressle.2 |
|
3 |
|
df-ple |
|
4 |
|
10nn |
|
5 |
|
1lt10 |
|
6 |
1 2 3 4 5
|
resslem |
|