Description: Closure for the interval endpoint function. (Contributed by Mario Carneiro, 16-Mar-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | ovolfcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffvelrn | |
|
2 | 1 | elin2d | |
3 | 1st2nd2 | |
|
4 | 2 3 | syl | |
5 | 4 1 | eqeltrrd | |
6 | ancom | |
|
7 | elin | |
|
8 | df-br | |
|
9 | 8 | bicomi | |
10 | opelxp | |
|
11 | 9 10 | anbi12i | |
12 | 7 11 | bitri | |
13 | df-3an | |
|
14 | 6 12 13 | 3bitr4i | |
15 | 5 14 | sylib | |