Description: The union of the range of the open interval function. (Contributed by NM, 7-May-2007) (Revised by Mario Carneiro, 30-Jan-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | unirnioo | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ioomax | |
|
2 | ioof | |
|
3 | ffn | |
|
4 | 2 3 | ax-mp | |
5 | mnfxr | |
|
6 | pnfxr | |
|
7 | fnovrn | |
|
8 | 4 5 6 7 | mp3an | |
9 | 1 8 | eqeltrri | |
10 | elssuni | |
|
11 | 9 10 | ax-mp | |
12 | frn | |
|
13 | 2 12 | ax-mp | |
14 | sspwuni | |
|
15 | 13 14 | mpbi | |
16 | 11 15 | eqssi | |