Metamath Proof Explorer

Theorem smflimsuplem1

Description: If H converges, the limsup of F is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smflimsuplem1.z 
|- Z = ( ZZ>= ` M )
smflimsuplem1.e 
|- E = ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
smflimsuplem1.h 
|- H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
smflimsuplem1.k 
|- ( ph -> K e. Z )
Assertion smflimsuplem1 
|- ( ph -> dom ( H ` K ) C_ dom ( F ` K ) )

Proof

Step Hyp Ref Expression
1 smflimsuplem1.z 
 |-  Z = ( ZZ>= ` M )
2 smflimsuplem1.e 
 |-  E = ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
3 smflimsuplem1.h 
 |-  H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
4 smflimsuplem1.k 
 |-  ( ph -> K e. Z )
5 fveq2 
 |-  ( m = j -> ( F ` m ) = ( F ` j ) )
6 5 fveq1d 
 |-  ( m = j -> ( ( F ` m ) ` x ) = ( ( F ` j ) ` x ) )
7 6 cbvmptv 
 |-  ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) = ( j e. ( ZZ>= ` n ) |-> ( ( F ` j ) ` x ) )
8 7 rneqi 
 |-  ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) = ran ( j e. ( ZZ>= ` n ) |-> ( ( F ` j ) ` x ) )
9 8 supeq1i 
 |-  sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) = sup ( ran ( j e. ( ZZ>= ` n ) |-> ( ( F ` j ) ` x ) ) , RR* , < )
10 9 mpteq2i 
 |-  ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) = ( x e. ( E ` n ) |-> sup ( ran ( j e. ( ZZ>= ` n ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) )
11 10 a1i 
 |-  ( n = K -> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) = ( x e. ( E ` n ) |-> sup ( ran ( j e. ( ZZ>= ` n ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) ) )
12 fveq2 
 |-  ( n = K -> ( E ` n ) = ( E ` K ) )
13 fveq2 
 |-  ( n = K -> ( ZZ>= ` n ) = ( ZZ>= ` K ) )
14 13 mpteq1d 
 |-  ( n = K -> ( j e. ( ZZ>= ` n ) |-> ( ( F ` j ) ` x ) ) = ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) )
15 14 rneqd 
 |-  ( n = K -> ran ( j e. ( ZZ>= ` n ) |-> ( ( F ` j ) ` x ) ) = ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) )
16 15 supeq1d 
 |-  ( n = K -> sup ( ran ( j e. ( ZZ>= ` n ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) = sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) )
17 12 16 mpteq12dv 
 |-  ( n = K -> ( x e. ( E ` n ) |-> sup ( ran ( j e. ( ZZ>= ` n ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) ) = ( x e. ( E ` K ) |-> sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) ) )
18 11 17 eqtrd 
 |-  ( n = K -> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) = ( x e. ( E ` K ) |-> sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) ) )
19 fvex 
 |-  ( E ` K ) e. _V
20 19 mptex 
 |-  ( x e. ( E ` K ) |-> sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) ) e. _V
21 20 a1i 
 |-  ( ph -> ( x e. ( E ` K ) |-> sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) ) e. _V )
22 3 18 4 21 fvmptd3 
 |-  ( ph -> ( H ` K ) = ( x e. ( E ` K ) |-> sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) ) )
23 22 dmeqd 
 |-  ( ph -> dom ( H ` K ) = dom ( x e. ( E ` K ) |-> sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) ) )
24 xrltso 
 |-  < Or RR*
25 24 supex 
 |-  sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. _V
26 eqid 
 |-  ( x e. ( E ` K ) |-> sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) ) = ( x e. ( E ` K ) |-> sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) )
27 25 26 dmmpti 
 |-  dom ( x e. ( E ` K ) |-> sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) ) = ( E ` K )
28 27 a1i 
 |-  ( ph -> dom ( x e. ( E ` K ) |-> sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) ) = ( E ` K ) )
29 5 dmeqd 
 |-  ( m = j -> dom ( F ` m ) = dom ( F ` j ) )
30 29 cbviinv 
 |-  |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = |^|_ j e. ( ZZ>= ` n ) dom ( F ` j )
31 30 eleq2i 
 |-  ( x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) <-> x e. |^|_ j e. ( ZZ>= ` n ) dom ( F ` j ) )
32 9 eleq1i 
 |-  ( sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR <-> sup ( ran ( j e. ( ZZ>= ` n ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR )
33 31 32 anbi12i 
 |-  ( ( x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR ) <-> ( x e. |^|_ j e. ( ZZ>= ` n ) dom ( F ` j ) /\ sup ( ran ( j e. ( ZZ>= ` n ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR ) )
34 33 rabbia2 
 |-  { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } = { x e. |^|_ j e. ( ZZ>= ` n ) dom ( F ` j ) | sup ( ran ( j e. ( ZZ>= ` n ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR }
35 34 a1i 
 |-  ( n = K -> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } = { x e. |^|_ j e. ( ZZ>= ` n ) dom ( F ` j ) | sup ( ran ( j e. ( ZZ>= ` n ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR } )
36 13 iineq1d 
 |-  ( n = K -> |^|_ j e. ( ZZ>= ` n ) dom ( F ` j ) = |^|_ j e. ( ZZ>= ` K ) dom ( F ` j ) )
37 36 eleq2d 
 |-  ( n = K -> ( x e. |^|_ j e. ( ZZ>= ` n ) dom ( F ` j ) <-> x e. |^|_ j e. ( ZZ>= ` K ) dom ( F ` j ) ) )
38 16 eleq1d 
 |-  ( n = K -> ( sup ( ran ( j e. ( ZZ>= ` n ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR <-> sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR ) )
39 37 38 anbi12d 
 |-  ( n = K -> ( ( x e. |^|_ j e. ( ZZ>= ` n ) dom ( F ` j ) /\ sup ( ran ( j e. ( ZZ>= ` n ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR ) <-> ( x e. |^|_ j e. ( ZZ>= ` K ) dom ( F ` j ) /\ sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR ) ) )
40 39 rabbidva2 
 |-  ( n = K -> { x e. |^|_ j e. ( ZZ>= ` n ) dom ( F ` j ) | sup ( ran ( j e. ( ZZ>= ` n ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR } = { x e. |^|_ j e. ( ZZ>= ` K ) dom ( F ` j ) | sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR } )
41 35 40 eqtrd 
 |-  ( n = K -> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } = { x e. |^|_ j e. ( ZZ>= ` K ) dom ( F ` j ) | sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR } )
42 eqid 
 |-  { x e. |^|_ j e. ( ZZ>= ` K ) dom ( F ` j ) | sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR } = { x e. |^|_ j e. ( ZZ>= ` K ) dom ( F ` j ) | sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR }
43 1 4 eluzelz2d 
 |-  ( ph -> K e. ZZ )
44 uzid 
 |-  ( K e. ZZ -> K e. ( ZZ>= ` K ) )
45 ne0i 
 |-  ( K e. ( ZZ>= ` K ) -> ( ZZ>= ` K ) =/= (/) )
46 43 44 45 3syl 
 |-  ( ph -> ( ZZ>= ` K ) =/= (/) )
47 fvex 
 |-  ( F ` j ) e. _V
48 47 dmex 
 |-  dom ( F ` j ) e. _V
49 48 rgenw 
 |-  A. j e. ( ZZ>= ` K ) dom ( F ` j ) e. _V
50 49 a1i 
 |-  ( ph -> A. j e. ( ZZ>= ` K ) dom ( F ` j ) e. _V )
51 46 50 iinexd 
 |-  ( ph -> |^|_ j e. ( ZZ>= ` K ) dom ( F ` j ) e. _V )
52 42 51 rabexd 
 |-  ( ph -> { x e. |^|_ j e. ( ZZ>= ` K ) dom ( F ` j ) | sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR } e. _V )
53 2 41 4 52 fvmptd3 
 |-  ( ph -> ( E ` K ) = { x e. |^|_ j e. ( ZZ>= ` K ) dom ( F ` j ) | sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR } )
54 23 28 53 3eqtrd 
 |-  ( ph -> dom ( H ` K ) = { x e. |^|_ j e. ( ZZ>= ` K ) dom ( F ` j ) | sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR } )
55 ssrab2 
 |-  { x e. |^|_ j e. ( ZZ>= ` K ) dom ( F ` j ) | sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR } C_ |^|_ j e. ( ZZ>= ` K ) dom ( F ` j )
56 55 a1i 
 |-  ( ph -> { x e. |^|_ j e. ( ZZ>= ` K ) dom ( F ` j ) | sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR } C_ |^|_ j e. ( ZZ>= ` K ) dom ( F ` j ) )
57 43 44 syl 
 |-  ( ph -> K e. ( ZZ>= ` K ) )
58 fveq2 
 |-  ( j = K -> ( F ` j ) = ( F ` K ) )
59 58 dmeqd 
 |-  ( j = K -> dom ( F ` j ) = dom ( F ` K ) )
60 ssid 
 |-  dom ( F ` K ) C_ dom ( F ` K )
61 60 a1i 
 |-  ( ph -> dom ( F ` K ) C_ dom ( F ` K ) )
62 57 59 61 iinssd 
 |-  ( ph -> |^|_ j e. ( ZZ>= ` K ) dom ( F ` j ) C_ dom ( F ` K ) )
63 56 62 sstrd 
 |-  ( ph -> { x e. |^|_ j e. ( ZZ>= ` K ) dom ( F ` j ) | sup ( ran ( j e. ( ZZ>= ` K ) |-> ( ( F ` j ) ` x ) ) , RR* , < ) e. RR } C_ dom ( F ` K ) )
64 54 63 eqsstrd 
 |-  ( ph -> dom ( H ` K ) C_ dom ( F ` K ) )