Metamath Proof Explorer

Theorem smflimsuplem3

Description: The limit of the ( Hn ) functions is sigma-measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smflimsuplem3.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
smflimsuplem3.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
smflimsuplem3.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smflimsuplem3.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
smflimsuplem3.e ⊢ 𝐸 = ( 𝑛 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
smflimsuplem3.h ⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
Assertion smflimsuplem3 ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑘 ∈ 𝑍 ∩ 𝑛 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐻 ‘ 𝑛 ) ∣ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ↦ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) ) ) ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 smflimsuplem3.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 smflimsuplem3.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 smflimsuplem3.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4 smflimsuplem3.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
5 smflimsuplem3.e ⊢ 𝐸 = ( 𝑛 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
6 smflimsuplem3.h ⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
7 nfv ⊢ Ⅎ 𝑛 𝜑
8 nfv ⊢ Ⅎ 𝑥 𝜑
9 nfv ⊢ Ⅎ 𝑘 𝜑
10 fvex ⊢ ( 𝐻 ‘ 𝑛 ) ∈ V
11 10 dmex ⊢ dom ( 𝐻 ‘ 𝑛 ) ∈ V
12 11 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → dom ( 𝐻 ‘ 𝑛 ) ∈ V )
13 fvexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐻 ‘ 𝑛 ) ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ∈ V )
14 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
15 5 a1i ⊢ ( 𝜑 → 𝐸 = ( 𝑛 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ) )
16 eqid ⊢ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ }
17 2 eluzelz2 ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ )
18 eqid ⊢ ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑛 )
19 17 18 uzn0d ⊢ ( 𝑛 ∈ 𝑍 → ( ℤ≥ ‘ 𝑛 ) ≠ ∅ )
20 fvex ⊢ ( 𝐹 ‘ 𝑚 ) ∈ V
21 20 dmex ⊢ dom ( 𝐹 ‘ 𝑚 ) ∈ V
22 21 rgenw ⊢ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V
23 22 a1i ⊢ ( 𝑛 ∈ 𝑍 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
24 19 23 iinexd ⊢ ( 𝑛 ∈ 𝑍 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
25 24 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
26 16 25 rabexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ∈ V )
27 15 26 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
28 fvres ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) = ( 𝐹 ‘ 𝑚 ) )
29 28 eqcomd ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) → ( 𝐹 ‘ 𝑚 ) = ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) )
30 29 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑚 ) = ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) )
31 30 dmeqd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → dom ( 𝐹 ‘ 𝑚 ) = dom ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) )
32 31 iineq2dv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) )
33 32 eleq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ↔ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ) )
34 29 fveq1d ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) )
35 34 mpteq2ia ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) )
36 35 rneqi ⊢ ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) )
37 36 supeq1i ⊢ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) = sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < )
38 37 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) = sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) )
39 38 eleq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ↔ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ) )
40 33 39 anbi12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ) ↔ ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ∧ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ) ) )
41 40 rabbidva2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
42 27 41 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
43 42 38 mpteq12dv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
44 nfcv ⊢ Ⅎ 𝑚 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) )
45 nfcv ⊢ Ⅎ 𝑥 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) )
46 17 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ ℤ )
47 4 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
48 2 eleq2i ⊢ ( 𝑛 ∈ 𝑍 ↔ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
49 48 biimpi ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
50 uzss ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑛 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
51 49 50 syl ⊢ ( 𝑛 ∈ 𝑍 → ( ℤ≥ ‘ 𝑛 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
52 51 2 sseqtrrdi ⊢ ( 𝑛 ∈ 𝑍 → ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 )
54 47 53 fssresd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) : ( ℤ≥ ‘ 𝑛 ) ⟶ ( SMblFn ‘ 𝑆 ) )
55 eqid ⊢ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ }
56 eqid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) )
57 44 45 46 18 14 54 55 56 smfsupxr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ∈ ( SMblFn ‘ 𝑆 ) )
58 43 57 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ∈ ( SMblFn ‘ 𝑆 ) )
59 58 6 fmptd ⊢ ( 𝜑 → 𝐻 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
60 59 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) ∈ ( SMblFn ‘ 𝑆 ) )
61 eqid ⊢ dom ( 𝐻 ‘ 𝑛 ) = dom ( 𝐻 ‘ 𝑛 )
62 14 60 61 smff ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) : dom ( 𝐻 ‘ 𝑛 ) ⟶ ℝ )
63 62 feqmptd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑥 ∈ dom ( 𝐻 ‘ 𝑛 ) ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) )
64 63 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ dom ( 𝐻 ‘ 𝑛 ) ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝐻 ‘ 𝑛 ) )
65 64 60 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ dom ( 𝐻 ‘ 𝑛 ) ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ ( SMblFn ‘ 𝑆 ) )
66 eqid ⊢ { 𝑥 ∈ ∪ 𝑘 ∈ 𝑍 ∩ 𝑛 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐻 ‘ 𝑛 ) ∣ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ dom ⇝ } = { 𝑥 ∈ ∪ 𝑘 ∈ 𝑍 ∩ 𝑛 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐻 ‘ 𝑛 ) ∣ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
67 eqid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑘 ∈ 𝑍 ∩ 𝑛 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐻 ‘ 𝑛 ) ∣ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ↦ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑘 ∈ 𝑍 ∩ 𝑛 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐻 ‘ 𝑛 ) ∣ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ↦ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) ) )
68 7 8 9 1 2 12 13 3 65 66 67 smflimmpt ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑘 ∈ 𝑍 ∩ 𝑛 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐻 ‘ 𝑛 ) ∣ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ↦ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) ) ) ∈ ( SMblFn ‘ 𝑆 ) )