Description: A sufficient condition for being an open set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | elrestd.1 | |
|
elrestd.2 | |
||
elrestd.3 | |
||
elrestd.4 | |
||
Assertion | elrestd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrestd.1 | |
|
2 | elrestd.2 | |
|
3 | elrestd.3 | |
|
4 | elrestd.4 | |
|
5 | 4 | a1i | |
6 | ineq1 | |
|
7 | 6 | rspceeqv | |
8 | 3 5 7 | syl2anc | |
9 | elrest | |
|
10 | 1 2 9 | syl2anc | |
11 | 8 10 | mpbird | |