Metamath Proof Explorer


Theorem limsuplt

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 limsuplt B F : B * A * lim sup F < A j G j < A

Proof

Step Hyp Ref Expression
1 limsupval.1 G = k sup F k +∞ * * <
2 1 limsuple B F : B * A * A lim sup F j A G j
3 2 notbid B F : B * A * ¬ A lim sup F ¬ j A G j
4 rexnal j ¬ A G j ¬ j A G j
5 3 4 bitr4di B F : B * A * ¬ A lim sup F j ¬ A G j
6 simp2 B F : B * A * F : B *
7 reex V
8 7 ssex B B V
9 8 3ad2ant1 B F : B * A * B V
10 xrex * V
11 10 a1i B F : B * A * * V
12 fex2 F : B * B V * V F V
13 6 9 11 12 syl3anc B F : B * A * F V
14 limsupcl F V lim sup F *
15 13 14 syl B F : B * A * lim sup F *
16 simp3 B F : B * A * A *
17 xrltnle lim sup F * A * lim sup F < A ¬ A lim sup F
18 15 16 17 syl2anc B F : B * A * lim sup F < A ¬ A lim sup F
19 1 limsupgf G : *
20 19 ffvelrni j G j *
21 xrltnle G j * A * G j < A ¬ A G j
22 20 16 21 syl2anr B F : B * A * j G j < A ¬ A G j
23 22 rexbidva B F : B * A * j G j < A j ¬ A G j
24 5 18 23 3bitr4d B F : B * A * lim sup F < A j G j < A