Metamath Proof Explorer

Theorem smflimsup

Description: The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of Fremlin1 p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smflimsup.n 
|- F/_ m F
smflimsup.x 
|- F/_ x F
smflimsup.m 
|- ( ph -> M e. ZZ )
smflimsup.z 
|- Z = ( ZZ>= ` M )
smflimsup.s 
|- ( ph -> S e. SAlg )
smflimsup.f 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smflimsup.d 
|- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }
smflimsup.g 
|- G = ( x e. D |-> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
Assertion smflimsup 
|- ( ph -> G e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 smflimsup.n 
 |-  F/_ m F
2 smflimsup.x 
 |-  F/_ x F
3 smflimsup.m 
 |-  ( ph -> M e. ZZ )
4 smflimsup.z 
 |-  Z = ( ZZ>= ` M )
5 smflimsup.s 
 |-  ( ph -> S e. SAlg )
6 smflimsup.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
7 smflimsup.d 
 |-  D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }
8 smflimsup.g 
 |-  G = ( x e. D |-> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
9 fveq2 
 |-  ( n = j -> ( ZZ>= ` n ) = ( ZZ>= ` j ) )
10 9 iineq1d 
 |-  ( n = j -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = |^|_ m e. ( ZZ>= ` j ) dom ( F ` m ) )
11 nfcv 
 |-  F/_ q dom ( F ` m )
12 nfcv 
 |-  F/_ m q
13 1 12 nffv 
 |-  F/_ m ( F ` q )
14 13 nfdm 
 |-  F/_ m dom ( F ` q )
15 fveq2 
 |-  ( m = q -> ( F ` m ) = ( F ` q ) )
16 15 dmeqd 
 |-  ( m = q -> dom ( F ` m ) = dom ( F ` q ) )
17 11 14 16 cbviin 
 |-  |^|_ m e. ( ZZ>= ` j ) dom ( F ` m ) = |^|_ q e. ( ZZ>= ` j ) dom ( F ` q )
18 17 a1i 
 |-  ( n = j -> |^|_ m e. ( ZZ>= ` j ) dom ( F ` m ) = |^|_ q e. ( ZZ>= ` j ) dom ( F ` q ) )
19 10 18 eqtrd 
 |-  ( n = j -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = |^|_ q e. ( ZZ>= ` j ) dom ( F ` q ) )
20 19 cbviunv 
 |-  U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = U_ j e. Z |^|_ q e. ( ZZ>= ` j ) dom ( F ` q )
21 20 eleq2i 
 |-  ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) <-> x e. U_ j e. Z |^|_ q e. ( ZZ>= ` j ) dom ( F ` q ) )
22 nfcv 
 |-  F/_ q ( ( F ` m ) ` x )
23 nfcv 
 |-  F/_ m x
24 13 23 nffv 
 |-  F/_ m ( ( F ` q ) ` x )
25 15 fveq1d 
 |-  ( m = q -> ( ( F ` m ) ` x ) = ( ( F ` q ) ` x ) )
26 22 24 25 cbvmpt 
 |-  ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( q e. Z |-> ( ( F ` q ) ` x ) )
27 26 fveq2i 
 |-  ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( limsup ` ( q e. Z |-> ( ( F ` q ) ` x ) ) )
28 27 eleq1i 
 |-  ( ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR <-> ( limsup ` ( q e. Z |-> ( ( F ` q ) ` x ) ) ) e. RR )
29 21 28 anbi12i 
 |-  ( ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) <-> ( x e. U_ j e. Z |^|_ q e. ( ZZ>= ` j ) dom ( F ` q ) /\ ( limsup ` ( q e. Z |-> ( ( F ` q ) ` x ) ) ) e. RR ) )
30 29 rabbia2 
 |-  { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } = { x e. U_ j e. Z |^|_ q e. ( ZZ>= ` j ) dom ( F ` q ) | ( limsup ` ( q e. Z |-> ( ( F ` q ) ` x ) ) ) e. RR }
31 nfcv 
 |-  F/_ x Z
32 nfcv 
 |-  F/_ x ( ZZ>= ` j )
33 nfcv 
 |-  F/_ x q
34 2 33 nffv 
 |-  F/_ x ( F ` q )
35 34 nfdm 
 |-  F/_ x dom ( F ` q )
36 32 35 nfiin 
 |-  F/_ x |^|_ q e. ( ZZ>= ` j ) dom ( F ` q )
37 31 36 nfiun 
 |-  F/_ x U_ j e. Z |^|_ q e. ( ZZ>= ` j ) dom ( F ` q )
38 nfcv 
 |-  F/_ w U_ j e. Z |^|_ q e. ( ZZ>= ` j ) dom ( F ` q )
39 nfv 
 |-  F/ w ( limsup ` ( q e. Z |-> ( ( F ` q ) ` x ) ) ) e. RR
40 nfcv 
 |-  F/_ x limsup
41 nfcv 
 |-  F/_ x w
42 34 41 nffv 
 |-  F/_ x ( ( F ` q ) ` w )
43 31 42 nfmpt 
 |-  F/_ x ( q e. Z |-> ( ( F ` q ) ` w ) )
44 40 43 nffv 
 |-  F/_ x ( limsup ` ( q e. Z |-> ( ( F ` q ) ` w ) ) )
45 nfcv 
 |-  F/_ x RR
46 44 45 nfel 
 |-  F/ x ( limsup ` ( q e. Z |-> ( ( F ` q ) ` w ) ) ) e. RR
47 fveq2 
 |-  ( x = w -> ( ( F ` q ) ` x ) = ( ( F ` q ) ` w ) )
48 47 mpteq2dv 
 |-  ( x = w -> ( q e. Z |-> ( ( F ` q ) ` x ) ) = ( q e. Z |-> ( ( F ` q ) ` w ) ) )
49 48 fveq2d 
 |-  ( x = w -> ( limsup ` ( q e. Z |-> ( ( F ` q ) ` x ) ) ) = ( limsup ` ( q e. Z |-> ( ( F ` q ) ` w ) ) ) )
50 49 eleq1d 
 |-  ( x = w -> ( ( limsup ` ( q e. Z |-> ( ( F ` q ) ` x ) ) ) e. RR <-> ( limsup ` ( q e. Z |-> ( ( F ` q ) ` w ) ) ) e. RR ) )
51 37 38 39 46 50 cbvrabw 
 |-  { x e. U_ j e. Z |^|_ q e. ( ZZ>= ` j ) dom ( F ` q ) | ( limsup ` ( q e. Z |-> ( ( F ` q ) ` x ) ) ) e. RR } = { w e. U_ j e. Z |^|_ q e. ( ZZ>= ` j ) dom ( F ` q ) | ( limsup ` ( q e. Z |-> ( ( F ` q ) ` w ) ) ) e. RR }
52 7 30 51 3eqtri 
 |-  D = { w e. U_ j e. Z |^|_ q e. ( ZZ>= ` j ) dom ( F ` q ) | ( limsup ` ( q e. Z |-> ( ( F ` q ) ` w ) ) ) e. RR }
53 27 mpteq2i 
 |-  ( x e. D |-> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) ) = ( x e. D |-> ( limsup ` ( q e. Z |-> ( ( F ` q ) ` x ) ) ) )
54 nfrab1 
 |-  F/_ x { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }
55 7 54 nfcxfr 
 |-  F/_ x D
56 nfcv 
 |-  F/_ w D
57 nfcv 
 |-  F/_ w ( limsup ` ( q e. Z |-> ( ( F ` q ) ` x ) ) )
58 55 56 57 44 49 cbvmptf 
 |-  ( x e. D |-> ( limsup ` ( q e. Z |-> ( ( F ` q ) ` x ) ) ) ) = ( w e. D |-> ( limsup ` ( q e. Z |-> ( ( F ` q ) ` w ) ) ) )
59 8 53 58 3eqtri 
 |-  G = ( w e. D |-> ( limsup ` ( q e. Z |-> ( ( F ` q ) ` w ) ) ) )
60 nfcv 
 |-  F/_ x ( ZZ>= ` i )
61 60 35 nfiin 
 |-  F/_ x |^|_ q e. ( ZZ>= ` i ) dom ( F ` q )
62 nfcv 
 |-  F/_ w |^|_ q e. ( ZZ>= ` i ) dom ( F ` q )
63 nfv 
 |-  F/ w sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR
64 60 42 nfmpt 
 |-  F/_ x ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` w ) )
65 64 nfrn 
 |-  F/_ x ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` w ) )
66 nfcv 
 |-  F/_ x RR*
67 nfcv 
 |-  F/_ x <
68 65 66 67 nfsup 
 |-  F/_ x sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` w ) ) , RR* , < )
69 68 45 nfel 
 |-  F/ x sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) e. RR
70 47 mpteq2dv 
 |-  ( x = w -> ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) = ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` w ) ) )
71 70 rneqd 
 |-  ( x = w -> ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) = ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` w ) ) )
72 71 supeq1d 
 |-  ( x = w -> sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) = sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) )
73 72 eleq1d 
 |-  ( x = w -> ( sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR <-> sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) e. RR ) )
74 61 62 63 69 73 cbvrabw 
 |-  { x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR } = { w e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) e. RR }
75 74 a1i 
 |-  ( i = k -> { x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR } = { w e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) e. RR } )
76 fveq2 
 |-  ( i = k -> ( ZZ>= ` i ) = ( ZZ>= ` k ) )
77 76 iineq1d 
 |-  ( i = k -> |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) = |^|_ q e. ( ZZ>= ` k ) dom ( F ` q ) )
78 77 eleq2d 
 |-  ( i = k -> ( w e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) <-> w e. |^|_ q e. ( ZZ>= ` k ) dom ( F ` q ) ) )
79 76 mpteq1d 
 |-  ( i = k -> ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` w ) ) = ( q e. ( ZZ>= ` k ) |-> ( ( F ` q ) ` w ) ) )
80 79 rneqd 
 |-  ( i = k -> ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` w ) ) = ran ( q e. ( ZZ>= ` k ) |-> ( ( F ` q ) ` w ) ) )
81 80 supeq1d 
 |-  ( i = k -> sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) = sup ( ran ( q e. ( ZZ>= ` k ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) )
82 81 eleq1d 
 |-  ( i = k -> ( sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) e. RR <-> sup ( ran ( q e. ( ZZ>= ` k ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) e. RR ) )
83 78 82 anbi12d 
 |-  ( i = k -> ( ( w e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) /\ sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) e. RR ) <-> ( w e. |^|_ q e. ( ZZ>= ` k ) dom ( F ` q ) /\ sup ( ran ( q e. ( ZZ>= ` k ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) e. RR ) ) )
84 83 rabbidva2 
 |-  ( i = k -> { w e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) e. RR } = { w e. |^|_ q e. ( ZZ>= ` k ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` k ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) e. RR } )
85 75 84 eqtrd 
 |-  ( i = k -> { x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR } = { w e. |^|_ q e. ( ZZ>= ` k ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` k ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) e. RR } )
86 85 cbvmptv 
 |-  ( i e. Z |-> { x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR } ) = ( k e. Z |-> { w e. |^|_ q e. ( ZZ>= ` k ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` k ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) e. RR } )
87 fveq2 
 |-  ( y = w -> ( ( F ` p ) ` y ) = ( ( F ` p ) ` w ) )
88 87 mpteq2dv 
 |-  ( y = w -> ( p e. ( ZZ>= ` l ) |-> ( ( F ` p ) ` y ) ) = ( p e. ( ZZ>= ` l ) |-> ( ( F ` p ) ` w ) ) )
89 88 rneqd 
 |-  ( y = w -> ran ( p e. ( ZZ>= ` l ) |-> ( ( F ` p ) ` y ) ) = ran ( p e. ( ZZ>= ` l ) |-> ( ( F ` p ) ` w ) ) )
90 89 supeq1d 
 |-  ( y = w -> sup ( ran ( p e. ( ZZ>= ` l ) |-> ( ( F ` p ) ` y ) ) , RR* , < ) = sup ( ran ( p e. ( ZZ>= ` l ) |-> ( ( F ` p ) ` w ) ) , RR* , < ) )
91 90 cbvmptv 
 |-  ( y e. ( ( i e. Z |-> { x e. |^|_ p e. ( ZZ>= ` i ) dom ( F ` p ) | sup ( ran ( p e. ( ZZ>= ` i ) |-> ( ( F ` p ) ` x ) ) , RR* , < ) e. RR } ) ` l ) |-> sup ( ran ( p e. ( ZZ>= ` l ) |-> ( ( F ` p ) ` y ) ) , RR* , < ) ) = ( w e. ( ( i e. Z |-> { x e. |^|_ p e. ( ZZ>= ` i ) dom ( F ` p ) | sup ( ran ( p e. ( ZZ>= ` i ) |-> ( ( F ` p ) ` x ) ) , RR* , < ) e. RR } ) ` l ) |-> sup ( ran ( p e. ( ZZ>= ` l ) |-> ( ( F ` p ) ` w ) ) , RR* , < ) )
92 fveq2 
 |-  ( p = q -> ( F ` p ) = ( F ` q ) )
93 92 dmeqd 
 |-  ( p = q -> dom ( F ` p ) = dom ( F ` q ) )
94 93 cbviinv 
 |-  |^|_ p e. ( ZZ>= ` i ) dom ( F ` p ) = |^|_ q e. ( ZZ>= ` i ) dom ( F ` q )
95 94 eleq2i 
 |-  ( x e. |^|_ p e. ( ZZ>= ` i ) dom ( F ` p ) <-> x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) )
96 nfcv 
 |-  F/_ q ( ( F ` p ) ` x )
97 nfcv 
 |-  F/_ p ( F ` q )
98 nfcv 
 |-  F/_ p x
99 97 98 nffv 
 |-  F/_ p ( ( F ` q ) ` x )
100 92 fveq1d 
 |-  ( p = q -> ( ( F ` p ) ` x ) = ( ( F ` q ) ` x ) )
101 96 99 100 cbvmpt 
 |-  ( p e. ( ZZ>= ` i ) |-> ( ( F ` p ) ` x ) ) = ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) )
102 101 rneqi 
 |-  ran ( p e. ( ZZ>= ` i ) |-> ( ( F ` p ) ` x ) ) = ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) )
103 102 supeq1i 
 |-  sup ( ran ( p e. ( ZZ>= ` i ) |-> ( ( F ` p ) ` x ) ) , RR* , < ) = sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < )
104 103 eleq1i 
 |-  ( sup ( ran ( p e. ( ZZ>= ` i ) |-> ( ( F ` p ) ` x ) ) , RR* , < ) e. RR <-> sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR )
105 95 104 anbi12i 
 |-  ( ( x e. |^|_ p e. ( ZZ>= ` i ) dom ( F ` p ) /\ sup ( ran ( p e. ( ZZ>= ` i ) |-> ( ( F ` p ) ` x ) ) , RR* , < ) e. RR ) <-> ( x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) /\ sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR ) )
106 105 rabbia2 
 |-  { x e. |^|_ p e. ( ZZ>= ` i ) dom ( F ` p ) | sup ( ran ( p e. ( ZZ>= ` i ) |-> ( ( F ` p ) ` x ) ) , RR* , < ) e. RR } = { x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR }
107 106 mpteq2i 
 |-  ( i e. Z |-> { x e. |^|_ p e. ( ZZ>= ` i ) dom ( F ` p ) | sup ( ran ( p e. ( ZZ>= ` i ) |-> ( ( F ` p ) ` x ) ) , RR* , < ) e. RR } ) = ( i e. Z |-> { x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR } )
108 107 fveq1i 
 |-  ( ( i e. Z |-> { x e. |^|_ p e. ( ZZ>= ` i ) dom ( F ` p ) | sup ( ran ( p e. ( ZZ>= ` i ) |-> ( ( F ` p ) ` x ) ) , RR* , < ) e. RR } ) ` l ) = ( ( i e. Z |-> { x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR } ) ` l )
109 92 fveq1d 
 |-  ( p = q -> ( ( F ` p ) ` w ) = ( ( F ` q ) ` w ) )
110 109 cbvmptv 
 |-  ( p e. ( ZZ>= ` l ) |-> ( ( F ` p ) ` w ) ) = ( q e. ( ZZ>= ` l ) |-> ( ( F ` q ) ` w ) )
111 110 rneqi 
 |-  ran ( p e. ( ZZ>= ` l ) |-> ( ( F ` p ) ` w ) ) = ran ( q e. ( ZZ>= ` l ) |-> ( ( F ` q ) ` w ) )
112 111 supeq1i 
 |-  sup ( ran ( p e. ( ZZ>= ` l ) |-> ( ( F ` p ) ` w ) ) , RR* , < ) = sup ( ran ( q e. ( ZZ>= ` l ) |-> ( ( F ` q ) ` w ) ) , RR* , < )
113 108 112 mpteq12i 
 |-  ( w e. ( ( i e. Z |-> { x e. |^|_ p e. ( ZZ>= ` i ) dom ( F ` p ) | sup ( ran ( p e. ( ZZ>= ` i ) |-> ( ( F ` p ) ` x ) ) , RR* , < ) e. RR } ) ` l ) |-> sup ( ran ( p e. ( ZZ>= ` l ) |-> ( ( F ` p ) ` w ) ) , RR* , < ) ) = ( w e. ( ( i e. Z |-> { x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR } ) ` l ) |-> sup ( ran ( q e. ( ZZ>= ` l ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) )
114 91 113 eqtri 
 |-  ( y e. ( ( i e. Z |-> { x e. |^|_ p e. ( ZZ>= ` i ) dom ( F ` p ) | sup ( ran ( p e. ( ZZ>= ` i ) |-> ( ( F ` p ) ` x ) ) , RR* , < ) e. RR } ) ` l ) |-> sup ( ran ( p e. ( ZZ>= ` l ) |-> ( ( F ` p ) ` y ) ) , RR* , < ) ) = ( w e. ( ( i e. Z |-> { x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR } ) ` l ) |-> sup ( ran ( q e. ( ZZ>= ` l ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) )
115 114 a1i 
 |-  ( l = k -> ( y e. ( ( i e. Z |-> { x e. |^|_ p e. ( ZZ>= ` i ) dom ( F ` p ) | sup ( ran ( p e. ( ZZ>= ` i ) |-> ( ( F ` p ) ` x ) ) , RR* , < ) e. RR } ) ` l ) |-> sup ( ran ( p e. ( ZZ>= ` l ) |-> ( ( F ` p ) ` y ) ) , RR* , < ) ) = ( w e. ( ( i e. Z |-> { x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR } ) ` l ) |-> sup ( ran ( q e. ( ZZ>= ` l ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) ) )
116 fveq2 
 |-  ( l = k -> ( ( i e. Z |-> { x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR } ) ` l ) = ( ( i e. Z |-> { x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR } ) ` k ) )
117 fveq2 
 |-  ( l = k -> ( ZZ>= ` l ) = ( ZZ>= ` k ) )
118 117 mpteq1d 
 |-  ( l = k -> ( q e. ( ZZ>= ` l ) |-> ( ( F ` q ) ` w ) ) = ( q e. ( ZZ>= ` k ) |-> ( ( F ` q ) ` w ) ) )
119 118 rneqd 
 |-  ( l = k -> ran ( q e. ( ZZ>= ` l ) |-> ( ( F ` q ) ` w ) ) = ran ( q e. ( ZZ>= ` k ) |-> ( ( F ` q ) ` w ) ) )
120 119 supeq1d 
 |-  ( l = k -> sup ( ran ( q e. ( ZZ>= ` l ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) = sup ( ran ( q e. ( ZZ>= ` k ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) )
121 116 120 mpteq12dv 
 |-  ( l = k -> ( w e. ( ( i e. Z |-> { x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR } ) ` l ) |-> sup ( ran ( q e. ( ZZ>= ` l ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) ) = ( w e. ( ( i e. Z |-> { x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR } ) ` k ) |-> sup ( ran ( q e. ( ZZ>= ` k ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) ) )
122 115 121 eqtrd 
 |-  ( l = k -> ( y e. ( ( i e. Z |-> { x e. |^|_ p e. ( ZZ>= ` i ) dom ( F ` p ) | sup ( ran ( p e. ( ZZ>= ` i ) |-> ( ( F ` p ) ` x ) ) , RR* , < ) e. RR } ) ` l ) |-> sup ( ran ( p e. ( ZZ>= ` l ) |-> ( ( F ` p ) ` y ) ) , RR* , < ) ) = ( w e. ( ( i e. Z |-> { x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR } ) ` k ) |-> sup ( ran ( q e. ( ZZ>= ` k ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) ) )
123 122 cbvmptv 
 |-  ( l e. Z |-> ( y e. ( ( i e. Z |-> { x e. |^|_ p e. ( ZZ>= ` i ) dom ( F ` p ) | sup ( ran ( p e. ( ZZ>= ` i ) |-> ( ( F ` p ) ` x ) ) , RR* , < ) e. RR } ) ` l ) |-> sup ( ran ( p e. ( ZZ>= ` l ) |-> ( ( F ` p ) ` y ) ) , RR* , < ) ) ) = ( k e. Z |-> ( w e. ( ( i e. Z |-> { x e. |^|_ q e. ( ZZ>= ` i ) dom ( F ` q ) | sup ( ran ( q e. ( ZZ>= ` i ) |-> ( ( F ` q ) ` x ) ) , RR* , < ) e. RR } ) ` k ) |-> sup ( ran ( q e. ( ZZ>= ` k ) |-> ( ( F ` q ) ` w ) ) , RR* , < ) ) )
124 3 4 5 6 52 59 86 123 smflimsuplem8 
 |-  ( ph -> G e. ( SMblFn ` S ) )