Description: D is a function that returns the representation of the left side of the difference of a half-open interval and a half-space. Used in Lemma 115F of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hoidifhspval.d | |
|
hoidifhspval.y | |
||
Assertion | hoidifhspval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hoidifhspval.d | |
|
2 | hoidifhspval.y | |
|
3 | breq1 | |
|
4 | id | |
|
5 | 3 4 | ifbieq2d | |
6 | 5 | ifeq1d | |
7 | 6 | mpteq2dv | |
8 | 7 | mpteq2dv | |
9 | ovex | |
|
10 | 9 | mptex | |
11 | 10 | a1i | |
12 | 1 8 2 11 | fvmptd3 | |