Metamath Proof Explorer

Theorem limsup0

Description: The superior limit of the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion limsup0 
|- ( limsup ` (/) ) = -oo

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 eqid 
 |-  ( x e. RR |-> sup ( ( ( (/) " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( x e. RR |-> sup ( ( ( (/) " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) )
3 2 limsupval 
 |-  ( (/) e. _V -> ( limsup ` (/) ) = inf ( ran ( x e. RR |-> sup ( ( ( (/) " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
4 1 3 ax-mp 
 |-  ( limsup ` (/) ) = inf ( ran ( x e. RR |-> sup ( ( ( (/) " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < )
5 0ima 
 |-  ( (/) " ( x [,) +oo ) ) = (/)
6 5 ineq1i 
 |-  ( ( (/) " ( x [,) +oo ) ) i^i RR* ) = ( (/) i^i RR* )
7 0in 
 |-  ( (/) i^i RR* ) = (/)
8 6 7 eqtri 
 |-  ( ( (/) " ( x [,) +oo ) ) i^i RR* ) = (/)
9 8 supeq1i 
 |-  sup ( ( ( (/) " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) = sup ( (/) , RR* , < )
10 xrsup0 
 |-  sup ( (/) , RR* , < ) = -oo
11 9 10 eqtri 
 |-  sup ( ( ( (/) " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) = -oo
12 11 mpteq2i 
 |-  ( x e. RR |-> sup ( ( ( (/) " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( x e. RR |-> -oo )
13 ren0 
 |-  RR =/= (/)
14 13 a1i 
 |-  ( T. -> RR =/= (/) )
15 12 14 rnmptc 
 |-  ( T. -> ran ( x e. RR |-> sup ( ( ( (/) " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) ) = { -oo } )
16 15 mptru 
 |-  ran ( x e. RR |-> sup ( ( ( (/) " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) ) = { -oo }
17 16 infeq1i 
 |-  inf ( ran ( x e. RR |-> sup ( ( ( (/) " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) = inf ( { -oo } , RR* , < )
18 xrltso 
 |-  < Or RR*
19 mnfxr 
 |-  -oo e. RR*
20 infsn 
 |-  ( ( < Or RR* /\ -oo e. RR* ) -> inf ( { -oo } , RR* , < ) = -oo )
21 18 19 20 mp2an 
 |-  inf ( { -oo } , RR* , < ) = -oo
22 4 17 21 3eqtri 
 |-  ( limsup ` (/) ) = -oo