Metamath Proof Explorer

Theorem smflimsuplem7

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 smflimsuplem7.m 
|- ( ph -> M e. ZZ )
smflimsuplem7.z 
|- Z = ( ZZ>= ` M )
smflimsuplem7.s 
|- ( ph -> S e. SAlg )
smflimsuplem7.f 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smflimsuplem7.d 
|- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }
smflimsuplem7.e 
|- E = ( k e. Z |-> { x e. |^|_ m e. ( ZZ>= ` k ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
smflimsuplem7.h 
|- H = ( k e. Z |-> ( x e. ( E ` k ) |-> sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
Assertion smflimsuplem7 
|- ( ph -> D = { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } )

Proof

Step Hyp Ref Expression
1 smflimsuplem7.m 
 |-  ( ph -> M e. ZZ )
2 smflimsuplem7.z 
 |-  Z = ( ZZ>= ` M )
3 smflimsuplem7.s 
 |-  ( ph -> S e. SAlg )
4 smflimsuplem7.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
5 smflimsuplem7.d 
 |-  D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }
6 smflimsuplem7.e 
 |-  E = ( k e. Z |-> { x e. |^|_ m e. ( ZZ>= ` k ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
7 smflimsuplem7.h 
 |-  H = ( k e. Z |-> ( x e. ( E ` k ) |-> sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
8 5 a1i 
 |-  ( ph -> D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } )
9 simpl 
 |-  ( ( ph /\ x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } ) -> ph )
10 rabidim2 
 |-  ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
11 10 adantl 
 |-  ( ( ph /\ x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } ) -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
12 rabidim1 
 |-  ( x e. { 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_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
13 eliun 
 |-  ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) <-> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
14 12 13 sylib 
 |-  ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
15 14 adantl 
 |-  ( ( ph /\ x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } ) -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
16 nfv 
 |-  F/ n ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
17 nfv 
 |-  F/ m ph
18 nfcv 
 |-  F/_ m limsup
19 nfmpt1 
 |-  F/_ m ( m e. Z |-> ( ( F ` m ) ` x ) )
20 18 19 nffv 
 |-  F/_ m ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) )
21 nfcv 
 |-  F/_ m RR
22 20 21 nfel 
 |-  F/ m ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR
23 17 22 nfan 
 |-  F/ m ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
24 nfv 
 |-  F/ m n e. Z
25 nfcv 
 |-  F/_ m x
26 nfii1 
 |-  F/_ m |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
27 25 26 nfel 
 |-  F/ m x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
28 23 24 27 nf3an 
 |-  F/ m ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
29 nfv 
 |-  F/ m k e. ( ZZ>= ` n )
30 28 29 nfan 
 |-  F/ m ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ k e. ( ZZ>= ` n ) )
31 simpl1l 
 |-  ( ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ k e. ( ZZ>= ` n ) ) -> ph )
32 31 1 syl 
 |-  ( ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ k e. ( ZZ>= ` n ) ) -> M e. ZZ )
33 31 3 syl 
 |-  ( ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ k e. ( ZZ>= ` n ) ) -> S e. SAlg )
34 31 4 syl 
 |-  ( ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ k e. ( ZZ>= ` n ) ) -> F : Z --> ( SMblFn ` S ) )
35 2 uztrn2 
 |-  ( ( n e. Z /\ k e. ( ZZ>= ` n ) ) -> k e. Z )
36 35 3ad2antl2 
 |-  ( ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ k e. ( ZZ>= ` n ) ) -> k e. Z )
37 simpl1r 
 |-  ( ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ k e. ( ZZ>= ` n ) ) -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
38 uzss 
 |-  ( k e. ( ZZ>= ` n ) -> ( ZZ>= ` k ) C_ ( ZZ>= ` n ) )
39 iinss1 
 |-  ( ( ZZ>= ` k ) C_ ( ZZ>= ` n ) -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) C_ |^|_ m e. ( ZZ>= ` k ) dom ( F ` m ) )
40 38 39 syl 
 |-  ( k e. ( ZZ>= ` n ) -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) C_ |^|_ m e. ( ZZ>= ` k ) dom ( F ` m ) )
41 40 adantl 
 |-  ( ( x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ k e. ( ZZ>= ` n ) ) -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) C_ |^|_ m e. ( ZZ>= ` k ) dom ( F ` m ) )
42 simpl 
 |-  ( ( x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ k e. ( ZZ>= ` n ) ) -> x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
43 41 42 sseldd 
 |-  ( ( x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ k e. ( ZZ>= ` n ) ) -> x e. |^|_ m e. ( ZZ>= ` k ) dom ( F ` m ) )
44 43 3ad2antl3 
 |-  ( ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ k e. ( ZZ>= ` n ) ) -> x e. |^|_ m e. ( ZZ>= ` k ) dom ( F ` m ) )
45 30 32 2 33 34 6 7 36 37 44 smflimsuplem2 
 |-  ( ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ k e. ( ZZ>= ` n ) ) -> x e. dom ( H ` k ) )
46 45 ralrimiva 
 |-  ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> A. k e. ( ZZ>= ` n ) x e. dom ( H ` k ) )
47 vex 
 |-  x e. _V
48 eliin 
 |-  ( x e. _V -> ( x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) <-> A. k e. ( ZZ>= ` n ) x e. dom ( H ` k ) ) )
49 47 48 ax-mp 
 |-  ( x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) <-> A. k e. ( ZZ>= ` n ) x e. dom ( H ` k ) )
50 46 49 sylibr 
 |-  ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) )
51 50 3exp 
 |-  ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) -> ( n e. Z -> ( x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) -> x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) ) ) )
52 16 51 reximdai 
 |-  ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) -> ( E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) -> E. n e. Z x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) ) )
53 52 imp 
 |-  ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> E. n e. Z x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) )
54 eliun 
 |-  ( x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) <-> E. n e. Z x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) )
55 53 54 sylibr 
 |-  ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) )
56 9 11 15 55 syl21anc 
 |-  ( ( ph /\ x e. { 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_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) )
57 13 biimpi 
 |-  ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
58 12 57 syl 
 |-  ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
59 58 adantl 
 |-  ( ( ph /\ x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } ) -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
60 nfv 
 |-  F/ n ph
61 nfcv 
 |-  F/_ n x
62 nfv 
 |-  F/ n ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR
63 nfiu1 
 |-  F/_ n U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
64 62 63 nfrabw 
 |-  F/_ n { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }
65 61 64 nfel 
 |-  F/ n x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }
66 60 65 nfan 
 |-  F/ n ( ph /\ x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } )
67 nfv 
 |-  F/ n ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~>
68 nfv 
 |-  F/ k ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
69 simp1l 
 |-  ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ph )
70 69 1 syl 
 |-  ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> M e. ZZ )
71 69 3 syl 
 |-  ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> S e. SAlg )
72 69 4 syl 
 |-  ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> F : Z --> ( SMblFn ` S ) )
73 simp1r 
 |-  ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
74 simp2 
 |-  ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> n e. Z )
75 simp3 
 |-  ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
76 68 28 70 2 71 72 6 7 73 74 75 smflimsuplem6 
 |-  ( ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> )
77 76 3exp 
 |-  ( ( ph /\ ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) -> ( n e. Z -> ( x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) -> ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> ) ) )
78 11 77 syldan 
 |-  ( ( ph /\ x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } ) -> ( n e. Z -> ( x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) -> ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> ) ) )
79 66 67 78 rexlimd 
 |-  ( ( ph /\ x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } ) -> ( E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) -> ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> ) )
80 59 79 mpd 
 |-  ( ( ph /\ x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } ) -> ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> )
81 56 80 jca 
 |-  ( ( ph /\ x e. { 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_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) /\ ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> ) )
82 rabid 
 |-  ( x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } <-> ( x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) /\ ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> ) )
83 81 82 sylibr 
 |-  ( ( ph /\ x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } ) -> x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } )
84 83 ex 
 |-  ( ph -> ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } -> x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } ) )
85 ssrab2 
 |-  { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } C_ U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k )
86 85 a1i 
 |-  ( ph -> { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } C_ U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) )
87 2 eluzelz2 
 |-  ( n e. Z -> n e. ZZ )
88 87 uzidd 
 |-  ( n e. Z -> n e. ( ZZ>= ` n ) )
89 88 adantl 
 |-  ( ( ph /\ n e. Z ) -> n e. ( ZZ>= ` n ) )
90 nfv 
 |-  F/ x ( ph /\ n e. Z )
91 xrltso 
 |-  < Or RR*
92 91 a1i 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( E ` n ) ) -> < Or RR* )
93 92 supexd 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( E ` n ) ) -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. _V )
94 eqid 
 |-  ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) = ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) )
95 90 93 94 fnmptd 
 |-  ( ( ph /\ n e. Z ) -> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) Fn ( E ` n ) )
96 fveq2 
 |-  ( k = n -> ( E ` k ) = ( E ` n ) )
97 fveq2 
 |-  ( k = n -> ( ZZ>= ` k ) = ( ZZ>= ` n ) )
98 97 mpteq1d 
 |-  ( k = n -> ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) = ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) )
99 98 rneqd 
 |-  ( k = n -> ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) = ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) )
100 99 supeq1d 
 |-  ( k = n -> sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) )
101 96 100 mpteq12dv 
 |-  ( k = n -> ( x e. ( E ` k ) |-> sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) = ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
102 fvex 
 |-  ( E ` n ) e. _V
103 102 mptex 
 |-  ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) e. _V
104 101 7 103 fvmpt 
 |-  ( n e. Z -> ( H ` n ) = ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
105 104 adantl 
 |-  ( ( ph /\ n e. Z ) -> ( H ` n ) = ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
106 105 fneq1d 
 |-  ( ( ph /\ n e. Z ) -> ( ( H ` n ) Fn ( E ` n ) <-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) Fn ( E ` n ) ) )
107 95 106 mpbird 
 |-  ( ( ph /\ n e. Z ) -> ( H ` n ) Fn ( E ` n ) )
108 107 fndmd 
 |-  ( ( ph /\ n e. Z ) -> dom ( H ` n ) = ( E ` n ) )
109 97 iineq1d 
 |-  ( k = n -> |^|_ m e. ( ZZ>= ` k ) dom ( F ` m ) = |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
110 109 eleq2d 
 |-  ( k = n -> ( x e. |^|_ m e. ( ZZ>= ` k ) dom ( F ` m ) <-> x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) )
111 100 eleq1d 
 |-  ( k = n -> ( sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR <-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR ) )
112 110 111 anbi12d 
 |-  ( k = n -> ( ( x e. |^|_ m e. ( ZZ>= ` k ) dom ( F ` m ) /\ sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR ) <-> ( x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR ) ) )
113 112 rabbidva2 
 |-  ( k = n -> { x e. |^|_ m e. ( ZZ>= ` k ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
114 id 
 |-  ( n e. Z -> n e. Z )
115 fveq2 
 |-  ( x = y -> ( ( F ` m ) ` x ) = ( ( F ` m ) ` y ) )
116 115 mpteq2dv 
 |-  ( x = y -> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) = ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) )
117 116 rneqd 
 |-  ( x = y -> ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) = ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) )
118 117 supeq1d 
 |-  ( x = y -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) )
119 118 eleq1d 
 |-  ( x = y -> ( sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR <-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) e. RR ) )
120 119 cbvrabv 
 |-  { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } = { y e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) e. RR }
121 88 ne0d 
 |-  ( n e. Z -> ( ZZ>= ` n ) =/= (/) )
122 fvex 
 |-  ( F ` m ) e. _V
123 122 dmex 
 |-  dom ( F ` m ) e. _V
124 123 rgenw 
 |-  A. m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V
125 124 a1i 
 |-  ( n e. Z -> A. m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V )
126 121 125 iinexd 
 |-  ( n e. Z -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V )
127 120 126 rabexd 
 |-  ( n e. Z -> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } e. _V )
128 6 113 114 127 fvmptd3 
 |-  ( n e. Z -> ( E ` n ) = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
129 128 adantl 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
130 ssrab2 
 |-  { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
131 130 a1i 
 |-  ( ( ph /\ n e. Z ) -> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
132 129 131 eqsstrd 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
133 108 132 eqsstrd 
 |-  ( ( ph /\ n e. Z ) -> dom ( H ` n ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
134 fveq2 
 |-  ( k = n -> ( H ` k ) = ( H ` n ) )
135 134 dmeqd 
 |-  ( k = n -> dom ( H ` k ) = dom ( H ` n ) )
136 135 sseq1d 
 |-  ( k = n -> ( dom ( H ` k ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) <-> dom ( H ` n ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) )
137 136 rspcev 
 |-  ( ( n e. ( ZZ>= ` n ) /\ dom ( H ` n ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> E. k e. ( ZZ>= ` n ) dom ( H ` k ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
138 89 133 137 syl2anc 
 |-  ( ( ph /\ n e. Z ) -> E. k e. ( ZZ>= ` n ) dom ( H ` k ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
139 iinss 
 |-  ( E. k e. ( ZZ>= ` n ) dom ( H ` k ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) -> |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
140 138 139 syl 
 |-  ( ( ph /\ n e. Z ) -> |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
141 140 ralrimiva 
 |-  ( ph -> A. n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
142 ss2iun 
 |-  ( A. n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) -> U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
143 141 142 syl 
 |-  ( ph -> U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
144 86 143 sstrd 
 |-  ( ph -> { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
145 82 simplbi 
 |-  ( x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } -> x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) )
146 54 biimpi 
 |-  ( x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) -> E. n e. Z x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) )
147 145 146 syl 
 |-  ( x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } -> E. n e. Z x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) )
148 147 adantl 
 |-  ( ( ph /\ x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } ) -> E. n e. Z x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) )
149 nfiu1 
 |-  F/_ n U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k )
150 67 149 nfrabw 
 |-  F/_ n { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> }
151 61 150 nfel 
 |-  F/ n x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> }
152 60 151 nfan 
 |-  F/ n ( ph /\ x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } )
153 82 simprbi 
 |-  ( x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } -> ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> )
154 nfv 
 |-  F/ k ph
155 nfmpt1 
 |-  F/_ k ( k e. Z |-> ( ( H ` k ) ` x ) )
156 nfcv 
 |-  F/_ k dom ~~>
157 155 156 nfel 
 |-  F/ k ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~>
158 154 157 nfan 
 |-  F/ k ( ph /\ ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> )
159 nfv 
 |-  F/ k n e. Z
160 nfcv 
 |-  F/_ k x
161 nfii1 
 |-  F/_ k |^|_ k e. ( ZZ>= ` n ) dom ( H ` k )
162 160 161 nfel 
 |-  F/ k x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k )
163 158 159 162 nf3an 
 |-  F/ k ( ( ph /\ ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> ) /\ n e. Z /\ x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) )
164 1 adantr 
 |-  ( ( ph /\ n e. Z ) -> M e. ZZ )
165 164 3adant3 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) ) -> M e. ZZ )
166 165 3adant1r 
 |-  ( ( ( ph /\ ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> ) /\ n e. Z /\ x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) ) -> M e. ZZ )
167 3 adantr 
 |-  ( ( ph /\ n e. Z ) -> S e. SAlg )
168 167 3adant3 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) ) -> S e. SAlg )
169 168 3adant1r 
 |-  ( ( ( ph /\ ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> ) /\ n e. Z /\ x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) ) -> S e. SAlg )
170 4 adantr 
 |-  ( ( ph /\ n e. Z ) -> F : Z --> ( SMblFn ` S ) )
171 170 3adant3 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) ) -> F : Z --> ( SMblFn ` S ) )
172 171 3adant1r 
 |-  ( ( ( ph /\ ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> ) /\ n e. Z /\ x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) ) -> F : Z --> ( SMblFn ` S ) )
173 simp2 
 |-  ( ( ( ph /\ ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> ) /\ n e. Z /\ x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) ) -> n e. Z )
174 simp3 
 |-  ( ( ( ph /\ ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> ) /\ n e. Z /\ x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) ) -> x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) )
175 simp1r 
 |-  ( ( ( ph /\ ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> ) /\ n e. Z /\ x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) ) -> ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> )
176 163 166 2 169 172 6 7 173 174 175 smflimsuplem4 
 |-  ( ( ( ph /\ ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> ) /\ n e. Z /\ x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) ) -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
177 176 3exp 
 |-  ( ( ph /\ ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> ) -> ( n e. Z -> ( x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) ) )
178 153 177 sylan2 
 |-  ( ( ph /\ x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } ) -> ( n e. Z -> ( x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) ) )
179 152 62 178 rexlimd 
 |-  ( ( ph /\ x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } ) -> ( E. n e. Z x e. |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) )
180 148 179 mpd 
 |-  ( ( ph /\ x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } ) -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
181 180 ralrimiva 
 |-  ( ph -> A. x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
182 144 181 jca 
 |-  ( ph -> ( { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ A. x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) )
183 nfrab1 
 |-  F/_ x { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> }
184 nfcv 
 |-  F/_ x U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
185 183 184 ssrabf 
 |-  ( { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } C_ { 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_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ A. x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) )
186 182 185 sylibr 
 |-  ( ph -> { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } C_ { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } )
187 186 sseld 
 |-  ( ph -> ( x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } -> x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } ) )
188 84 187 impbid 
 |-  ( ph -> ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } <-> x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } ) )
189 188 alrimiv 
 |-  ( ph -> A. x ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } <-> x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } ) )
190 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 }
191 190 183 cleqf 
 |-  ( { 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_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } <-> A. x ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } <-> x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } ) )
192 189 191 sylibr 
 |-  ( ph -> { 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_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } )
193 8 192 eqtrd 
 |-  ( ph -> D = { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } )