Metamath Proof Explorer


Theorem limsuple

Description: The defining property of the superior limit. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

Ref Expression
Hypothesis limsupval.1 G = k sup F k +∞ * * <
Assertion limsuple B F : B * A * A lim sup F j A G j

Proof

Step Hyp Ref Expression
1 limsupval.1 G = k sup F k +∞ * * <
2 simp2 B F : B * A * F : B *
3 reex V
4 3 ssex B B V
5 4 3ad2ant1 B F : B * A * B V
6 xrex * V
7 6 a1i B F : B * A * * V
8 fex2 F : B * B V * V F V
9 2 5 7 8 syl3anc B F : B * A * F V
10 1 limsupval F V lim sup F = sup ran G * <
11 9 10 syl B F : B * A * lim sup F = sup ran G * <
12 11 breq2d B F : B * A * A lim sup F A sup ran G * <
13 1 limsupgf G : *
14 frn G : * ran G *
15 13 14 ax-mp ran G *
16 simp3 B F : B * A * A *
17 infxrgelb ran G * A * A sup ran G * < x ran G A x
18 15 16 17 sylancr B F : B * A * A sup ran G * < x ran G A x
19 ffn G : * G Fn
20 13 19 ax-mp G Fn
21 breq2 x = G j A x A G j
22 21 ralrn G Fn x ran G A x j A G j
23 20 22 ax-mp x ran G A x j A G j
24 18 23 bitrdi B F : B * A * A sup ran G * < j A G j
25 12 24 bitrd B F : B * A * A lim sup F j A G j