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 ⊢ Ⅎ 𝑚 𝐹
smflimsup.x ⊢ Ⅎ 𝑥 𝐹
smflimsup.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
smflimsup.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
smflimsup.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smflimsup.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
smflimsup.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ }
smflimsup.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
Assertion smflimsup ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 smflimsup.n ⊢ Ⅎ 𝑚 𝐹
2 smflimsup.x ⊢ Ⅎ 𝑥 𝐹
3 smflimsup.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 smflimsup.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5 smflimsup.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
6 smflimsup.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
7 smflimsup.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ }
8 smflimsup.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
9 fveq2 ⊢ ( 𝑛 = 𝑗 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑗 ) )
10 9 iineq1d ⊢ ( 𝑛 = 𝑗 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) dom ( 𝐹 ‘ 𝑚 ) )
11 nfcv ⊢ Ⅎ 𝑞 dom ( 𝐹 ‘ 𝑚 )
12 nfcv ⊢ Ⅎ 𝑚 𝑞
13 1 12 nffv ⊢ Ⅎ 𝑚 ( 𝐹 ‘ 𝑞 )
14 13 nfdm ⊢ Ⅎ 𝑚 dom ( 𝐹 ‘ 𝑞 )
15 fveq2 ⊢ ( 𝑚 = 𝑞 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑞 ) )
16 15 dmeqd ⊢ ( 𝑚 = 𝑞 → dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑞 ) )
17 11 14 16 cbviin ⊢ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑗 ) dom ( 𝐹 ‘ 𝑞 )
18 17 a1i ⊢ ( 𝑛 = 𝑗 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑗 ) dom ( 𝐹 ‘ 𝑞 ) )
19 10 18 eqtrd ⊢ ( 𝑛 = 𝑗 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑗 ) dom ( 𝐹 ‘ 𝑞 ) )
20 19 cbviunv ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∪ 𝑗 ∈ 𝑍 ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑗 ) dom ( 𝐹 ‘ 𝑞 )
21 20 eleq2i ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ↔ 𝑥 ∈ ∪ 𝑗 ∈ 𝑍 ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑗 ) dom ( 𝐹 ‘ 𝑞 ) )
22 nfcv ⊢ Ⅎ 𝑞 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 )
23 nfcv ⊢ Ⅎ 𝑚 𝑥
24 13 23 nffv ⊢ Ⅎ 𝑚 ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 )
25 15 fveq1d ⊢ ( 𝑚 = 𝑞 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) )
26 22 24 25 cbvmpt ⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) )
27 26 fveq2i ⊢ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) )
28 27 eleq1i ⊢ ( ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ↔ ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) ) ∈ ℝ )
29 21 28 anbi12i ⊢ ( ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ↔ ( 𝑥 ∈ ∪ 𝑗 ∈ 𝑍 ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑗 ) dom ( 𝐹 ‘ 𝑞 ) ∧ ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) ) ∈ ℝ ) )
30 29 rabbia2 ⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } = { 𝑥 ∈ ∪ 𝑗 ∈ 𝑍 ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑗 ) dom ( 𝐹 ‘ 𝑞 ) ∣ ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) ) ∈ ℝ }
31 nfcv ⊢ Ⅎ 𝑥 𝑍
32 nfcv ⊢ Ⅎ 𝑥 ( ℤ≥ ‘ 𝑗 )
33 nfcv ⊢ Ⅎ 𝑥 𝑞
34 2 33 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑞 )
35 34 nfdm ⊢ Ⅎ 𝑥 dom ( 𝐹 ‘ 𝑞 )
36 32 35 nfiin ⊢ Ⅎ 𝑥 ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑗 ) dom ( 𝐹 ‘ 𝑞 )
37 31 36 nfiun ⊢ Ⅎ 𝑥 ∪ 𝑗 ∈ 𝑍 ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑗 ) dom ( 𝐹 ‘ 𝑞 )
38 nfcv ⊢ Ⅎ 𝑤 ∪ 𝑗 ∈ 𝑍 ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑗 ) dom ( 𝐹 ‘ 𝑞 )
39 nfv ⊢ Ⅎ 𝑤 ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) ) ∈ ℝ
40 nfcv ⊢ Ⅎ 𝑥 lim sup
41 nfcv ⊢ Ⅎ 𝑥 𝑤
42 34 41 nffv ⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 )
43 31 42 nfmpt ⊢ Ⅎ 𝑥 ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) )
44 40 43 nffv ⊢ Ⅎ 𝑥 ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) )
45 nfcv ⊢ Ⅎ 𝑥 ℝ
46 44 45 nfel ⊢ Ⅎ 𝑥 ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) ) ∈ ℝ
47 fveq2 ⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) )
48 47 mpteq2dv ⊢ ( 𝑥 = 𝑤 → ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) = ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) )
49 48 fveq2d ⊢ ( 𝑥 = 𝑤 → ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) ) )
50 49 eleq1d ⊢ ( 𝑥 = 𝑤 → ( ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) ) ∈ ℝ ↔ ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) ) ∈ ℝ ) )
51 37 38 39 46 50 cbvrabw ⊢ { 𝑥 ∈ ∪ 𝑗 ∈ 𝑍 ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑗 ) dom ( 𝐹 ‘ 𝑞 ) ∣ ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) ) ∈ ℝ } = { 𝑤 ∈ ∪ 𝑗 ∈ 𝑍 ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑗 ) dom ( 𝐹 ‘ 𝑞 ) ∣ ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) ) ∈ ℝ }
52 7 30 51 3eqtri ⊢ 𝐷 = { 𝑤 ∈ ∪ 𝑗 ∈ 𝑍 ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑗 ) dom ( 𝐹 ‘ 𝑞 ) ∣ ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) ) ∈ ℝ }
53 27 mpteq2i ⊢ ( 𝑥 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) ) )
54 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ }
55 7 54 nfcxfr ⊢ Ⅎ 𝑥 𝐷
56 nfcv ⊢ Ⅎ 𝑤 𝐷
57 nfcv ⊢ Ⅎ 𝑤 ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) )
58 55 56 57 44 49 cbvmptf ⊢ ( 𝑥 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) ) ) = ( 𝑤 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) ) )
59 8 53 58 3eqtri ⊢ 𝐺 = ( 𝑤 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑞 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) ) )
60 nfcv ⊢ Ⅎ 𝑥 ( ℤ≥ ‘ 𝑖 )
61 60 35 nfiin ⊢ Ⅎ 𝑥 ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 )
62 nfcv ⊢ Ⅎ 𝑤 ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 )
63 nfv ⊢ Ⅎ 𝑤 sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ
64 60 42 nfmpt ⊢ Ⅎ 𝑥 ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) )
65 64 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) )
66 nfcv ⊢ Ⅎ 𝑥 ℝ*
67 nfcv ⊢ Ⅎ 𝑥 <
68 65 66 67 nfsup ⊢ Ⅎ 𝑥 sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < )
69 68 45 nfel ⊢ Ⅎ 𝑥 sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) ∈ ℝ
70 47 mpteq2dv ⊢ ( 𝑥 = 𝑤 → ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) = ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) )
71 70 rneqd ⊢ ( 𝑥 = 𝑤 → ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) = ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) )
72 71 supeq1d ⊢ ( 𝑥 = 𝑤 → sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) = sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) )
73 72 eleq1d ⊢ ( 𝑥 = 𝑤 → ( sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ↔ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) ∈ ℝ ) )
74 61 62 63 69 73 cbvrabw ⊢ { 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑤 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) ∈ ℝ }
75 74 a1i ⊢ ( 𝑖 = 𝑘 → { 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑤 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) ∈ ℝ } )
76 fveq2 ⊢ ( 𝑖 = 𝑘 → ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑘 ) )
77 76 iineq1d ⊢ ( 𝑖 = 𝑘 → ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) = ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑞 ) )
78 77 eleq2d ⊢ ( 𝑖 = 𝑘 → ( 𝑤 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ↔ 𝑤 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑞 ) ) )
79 76 mpteq1d ⊢ ( 𝑖 = 𝑘 → ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) = ( 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) )
80 79 rneqd ⊢ ( 𝑖 = 𝑘 → ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) = ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) )
81 80 supeq1d ⊢ ( 𝑖 = 𝑘 → sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) = sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) )
82 81 eleq1d ⊢ ( 𝑖 = 𝑘 → ( sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) ∈ ℝ ↔ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) ∈ ℝ ) )
83 78 82 anbi12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑤 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∧ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) ∈ ℝ ) ↔ ( 𝑤 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑞 ) ∧ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) ∈ ℝ ) ) )
84 83 rabbidva2 ⊢ ( 𝑖 = 𝑘 → { 𝑤 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑤 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) ∈ ℝ } )
85 75 84 eqtrd ⊢ ( 𝑖 = 𝑘 → { 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑤 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) ∈ ℝ } )
86 85 cbvmptv ⊢ ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) = ( 𝑘 ∈ 𝑍 ↦ { 𝑤 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) ∈ ℝ } )
87 fveq2 ⊢ ( 𝑦 = 𝑤 → ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑤 ) )
88 87 mpteq2dv ⊢ ( 𝑦 = 𝑤 → ( 𝑝 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑦 ) ) = ( 𝑝 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑤 ) ) )
89 88 rneqd ⊢ ( 𝑦 = 𝑤 → ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑦 ) ) = ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑤 ) ) )
90 89 supeq1d ⊢ ( 𝑦 = 𝑤 → sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑦 ) ) , ℝ* , < ) = sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑤 ) ) , ℝ* , < ) )
91 90 cbvmptv ⊢ ( 𝑦 ∈ ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑝 ) ∣ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑙 ) ↦ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑦 ) ) , ℝ* , < ) ) = ( 𝑤 ∈ ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑝 ) ∣ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑙 ) ↦ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑤 ) ) , ℝ* , < ) )
92 fveq2 ⊢ ( 𝑝 = 𝑞 → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) )
93 92 dmeqd ⊢ ( 𝑝 = 𝑞 → dom ( 𝐹 ‘ 𝑝 ) = dom ( 𝐹 ‘ 𝑞 ) )
94 93 cbviinv ⊢ ∩ 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑝 ) = ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 )
95 94 eleq2i ⊢ ( 𝑥 ∈ ∩ 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑝 ) ↔ 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) )
96 nfcv ⊢ Ⅎ 𝑞 ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑥 )
97 nfcv ⊢ Ⅎ 𝑝 ( 𝐹 ‘ 𝑞 )
98 nfcv ⊢ Ⅎ 𝑝 𝑥
99 97 98 nffv ⊢ Ⅎ 𝑝 ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 )
100 92 fveq1d ⊢ ( 𝑝 = 𝑞 → ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) )
101 96 99 100 cbvmpt ⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑥 ) ) = ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) )
102 101 rneqi ⊢ ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑥 ) ) = ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) )
103 102 supeq1i ⊢ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑥 ) ) , ℝ* , < ) = sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < )
104 103 eleq1i ⊢ ( sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ↔ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ )
105 95 104 anbi12i ⊢ ( ( 𝑥 ∈ ∩ 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑝 ) ∧ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ) ↔ ( 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∧ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ) )
106 105 rabbia2 ⊢ { 𝑥 ∈ ∩ 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑝 ) ∣ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ }
107 106 mpteq2i ⊢ ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑝 ) ∣ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) = ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
108 107 fveq1i ⊢ ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑝 ) ∣ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑙 ) = ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑙 )
109 92 fveq1d ⊢ ( 𝑝 = 𝑞 → ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑤 ) = ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) )
110 109 cbvmptv ⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑤 ) ) = ( 𝑞 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) )
111 110 rneqi ⊢ ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑤 ) ) = ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) )
112 111 supeq1i ⊢ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑤 ) ) , ℝ* , < ) = sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < )
113 108 112 mpteq12i ⊢ ( 𝑤 ∈ ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑝 ) ∣ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑙 ) ↦ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑤 ) ) , ℝ* , < ) ) = ( 𝑤 ∈ ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑙 ) ↦ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) )
114 91 113 eqtri ⊢ ( 𝑦 ∈ ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑝 ) ∣ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑙 ) ↦ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑦 ) ) , ℝ* , < ) ) = ( 𝑤 ∈ ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑙 ) ↦ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) )
115 114 a1i ⊢ ( 𝑙 = 𝑘 → ( 𝑦 ∈ ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑝 ) ∣ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑙 ) ↦ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑦 ) ) , ℝ* , < ) ) = ( 𝑤 ∈ ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑙 ) ↦ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) ) )
116 fveq2 ⊢ ( 𝑙 = 𝑘 → ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑙 ) = ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑘 ) )
117 fveq2 ⊢ ( 𝑙 = 𝑘 → ( ℤ≥ ‘ 𝑙 ) = ( ℤ≥ ‘ 𝑘 ) )
118 117 mpteq1d ⊢ ( 𝑙 = 𝑘 → ( 𝑞 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) = ( 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) )
119 118 rneqd ⊢ ( 𝑙 = 𝑘 → ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) = ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) )
120 119 supeq1d ⊢ ( 𝑙 = 𝑘 → sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) = sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) )
121 116 120 mpteq12dv ⊢ ( 𝑙 = 𝑘 → ( 𝑤 ∈ ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑙 ) ↦ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) ) = ( 𝑤 ∈ ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑘 ) ↦ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) ) )
122 115 121 eqtrd ⊢ ( 𝑙 = 𝑘 → ( 𝑦 ∈ ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑝 ) ∣ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑙 ) ↦ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑦 ) ) , ℝ* , < ) ) = ( 𝑤 ∈ ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑘 ) ↦ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) ) )
123 122 cbvmptv ⊢ ( 𝑙 ∈ 𝑍 ↦ ( 𝑦 ∈ ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑝 ) ∣ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑙 ) ↦ sup ( ran ( 𝑝 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ ( ( 𝐹 ‘ 𝑝 ) ‘ 𝑦 ) ) , ℝ* , < ) ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 𝑤 ∈ ( ( 𝑖 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑞 ) ∣ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) ‘ 𝑘 ) ↦ sup ( ran ( 𝑞 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ) , ℝ* , < ) ) )
124 3 4 5 6 52 59 86 123 smflimsuplem8 ⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )