Metamath Proof Explorer


Theorem unirnioo

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 =ran.

Proof

Step Hyp Ref Expression
1 ioomax −∞+∞=
2 ioof .:*×*𝒫
3 ffn .:*×*𝒫.Fn*×*
4 2 3 ax-mp .Fn*×*
5 mnfxr −∞*
6 pnfxr +∞*
7 fnovrn .Fn*×*−∞*+∞*−∞+∞ran.
8 4 5 6 7 mp3an −∞+∞ran.
9 1 8 eqeltrri ran.
10 elssuni ran.ran.
11 9 10 ax-mp ran.
12 frn .:*×*𝒫ran.𝒫
13 2 12 ax-mp ran.𝒫
14 sspwuni ran.𝒫ran.
15 13 14 mpbi ran.
16 11 15 eqssi =ran.