Metamath Proof Explorer

Theorem smflim

Description: The limit of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of Fremlin1 p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of Fremlin1 p. 39 ). (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smflim.n ⊢ Ⅎ 𝑚 𝐹
smflim.x ⊢ Ⅎ 𝑥 𝐹
smflim.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
smflim.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
smflim.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smflim.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
smflim.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
smflim.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
Assertion smflim ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 smflim.n ⊢ Ⅎ 𝑚 𝐹
2 smflim.x ⊢ Ⅎ 𝑥 𝐹
3 smflim.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 smflim.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5 smflim.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
6 smflim.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
7 smflim.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
8 smflim.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
9 nfv ⊢ Ⅎ 𝑎 𝜑
10 nfcv ⊢ Ⅎ 𝑥 𝑍
11 nfcv ⊢ Ⅎ 𝑥 ( ℤ≥ ‘ 𝑛 )
12 nfcv ⊢ Ⅎ 𝑥 𝑚
13 2 12 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑚 )
14 13 nfdm ⊢ Ⅎ 𝑥 dom ( 𝐹 ‘ 𝑚 )
15 11 14 nfiin ⊢ Ⅎ 𝑥 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
16 10 15 nfiun ⊢ Ⅎ 𝑥 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
17 16 ssrab2f ⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
18 7 17 eqsstri ⊢ 𝐷 ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
19 18 a1i ⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
20 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
21 4 eleq2i ⊢ ( 𝑛 ∈ 𝑍 ↔ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
22 21 biimpi ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
23 20 22 sselid ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ )
24 uzid ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
25 23 24 syl ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
26 25 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
27 5 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
28 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ( SMblFn ‘ 𝑆 ) )
29 eqid ⊢ dom ( 𝐹 ‘ 𝑛 ) = dom ( 𝐹 ‘ 𝑛 )
30 27 28 29 smfdmss ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → dom ( 𝐹 ‘ 𝑛 ) ⊆ ∪ 𝑆 )
31 nfcv ⊢ Ⅎ 𝑚 𝑛
32 1 31 nffv ⊢ Ⅎ 𝑚 ( 𝐹 ‘ 𝑛 )
33 32 nfdm ⊢ Ⅎ 𝑚 dom ( 𝐹 ‘ 𝑛 )
34 nfcv ⊢ Ⅎ 𝑚 ∪ 𝑆
35 33 34 nfss ⊢ Ⅎ 𝑚 dom ( 𝐹 ‘ 𝑛 ) ⊆ ∪ 𝑆
36 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) )
37 36 dmeqd ⊢ ( 𝑚 = 𝑛 → dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑛 ) )
38 37 sseq1d ⊢ ( 𝑚 = 𝑛 → ( dom ( 𝐹 ‘ 𝑚 ) ⊆ ∪ 𝑆 ↔ dom ( 𝐹 ‘ 𝑛 ) ⊆ ∪ 𝑆 ) )
39 35 38 rspce ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) ∧ dom ( 𝐹 ‘ 𝑛 ) ⊆ ∪ 𝑆 ) → ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∪ 𝑆 )
40 26 30 39 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∪ 𝑆 )
41 iinss ⊢ ( ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∪ 𝑆 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∪ 𝑆 )
42 40 41 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∪ 𝑆 )
43 42 iunssd ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∪ 𝑆 )
44 19 43 sstrd ⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
45 nfv ⊢ Ⅎ 𝑚 𝜑
46 nfcv ⊢ Ⅎ 𝑚 𝑦
47 nfmpt1 ⊢ Ⅎ 𝑚 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
48 nfcv ⊢ Ⅎ 𝑚 dom ⇝
49 47 48 nfel ⊢ Ⅎ 𝑚 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝
50 nfcv ⊢ Ⅎ 𝑚 𝑍
51 nfii1 ⊢ Ⅎ 𝑚 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
52 50 51 nfiun ⊢ Ⅎ 𝑚 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
53 49 52 nfrabw ⊢ Ⅎ 𝑚 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
54 7 53 nfcxfr ⊢ Ⅎ 𝑚 𝐷
55 46 54 nfel ⊢ Ⅎ 𝑚 𝑦 ∈ 𝐷
56 45 55 nfan ⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑦 ∈ 𝐷 )
57 nfcv ⊢ Ⅎ 𝑤 𝐹
58 5 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
59 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
60 eqid ⊢ dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑚 )
61 58 59 60 smff ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
62 61 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
63 nfcv ⊢ Ⅎ 𝑦 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
64 nfv ⊢ Ⅎ 𝑦 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝
65 nfcv ⊢ Ⅎ 𝑥 𝑦
66 13 65 nffv ⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 )
67 10 66 nfmpt ⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) )
68 67 nfel1 ⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝
69 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) )
70 69 mpteq2dv ⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) )
71 70 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ ) )
72 16 63 64 68 71 cbvrabw ⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } = { 𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ }
73 nfcv ⊢ Ⅎ 𝑙 dom ( 𝐹 ‘ 𝑚 )
74 nfcv ⊢ Ⅎ 𝑚 𝑙
75 1 74 nffv ⊢ Ⅎ 𝑚 ( 𝐹 ‘ 𝑙 )
76 75 nfdm ⊢ Ⅎ 𝑚 dom ( 𝐹 ‘ 𝑙 )
77 fveq2 ⊢ ( 𝑚 = 𝑙 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑙 ) )
78 77 dmeqd ⊢ ( 𝑚 = 𝑙 → dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑙 ) )
79 73 76 78 cbviin ⊢ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑙 )
80 79 a1i ⊢ ( 𝑛 = 𝑖 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑙 ) )
81 fveq2 ⊢ ( 𝑛 = 𝑖 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑖 ) )
82 eqidd ⊢ ( ( 𝑛 = 𝑖 ∧ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ) → dom ( 𝐹 ‘ 𝑙 ) = dom ( 𝐹 ‘ 𝑙 ) )
83 81 82 iineq12dv ⊢ ( 𝑛 = 𝑖 → ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑙 ) = ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) )
84 80 83 eqtrd ⊢ ( 𝑛 = 𝑖 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) )
85 84 cbviunv ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 )
86 85 eleq2i ⊢ ( 𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ↔ 𝑦 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) )
87 nfcv ⊢ Ⅎ 𝑙 𝑍
88 nfcv ⊢ Ⅎ 𝑙 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 )
89 75 46 nffv ⊢ Ⅎ 𝑚 ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 )
90 77 fveq1d ⊢ ( 𝑚 = 𝑙 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) )
91 50 87 88 89 90 cbvmptf ⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) = ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) )
92 91 eleq1i ⊢ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ ↔ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ∈ dom ⇝ )
93 86 92 anbi12i ⊢ ( ( 𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ ) ↔ ( 𝑦 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ∧ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ∈ dom ⇝ ) )
94 93 rabbia2 ⊢ { 𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ } = { 𝑦 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ∣ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ∈ dom ⇝ }
95 7 72 94 3eqtri ⊢ 𝐷 = { 𝑦 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ∣ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ∈ dom ⇝ }
96 fveq2 ⊢ ( 𝑦 = 𝑤 → ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) )
97 96 mpteq2dv ⊢ ( 𝑦 = 𝑤 → ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) = ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) ) )
98 97 eleq1d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ∈ dom ⇝ ↔ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) ) ∈ dom ⇝ ) )
99 98 cbvrabv ⊢ { 𝑦 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ∣ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ∈ dom ⇝ } = { 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ∣ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) ) ∈ dom ⇝ }
100 fveq2 ⊢ ( 𝑙 = 𝑚 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑚 ) )
101 100 dmeqd ⊢ ( 𝑙 = 𝑚 → dom ( 𝐹 ‘ 𝑙 ) = dom ( 𝐹 ‘ 𝑚 ) )
102 76 73 101 cbviin ⊢ ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 )
103 102 a1i ⊢ ( 𝑖 ∈ 𝑍 → ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
104 103 iuneq2i ⊢ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) = ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 )
105 104 eleq2i ⊢ ( 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ↔ 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
106 nfcv ⊢ Ⅎ 𝑚 𝑤
107 75 106 nffv ⊢ Ⅎ 𝑚 ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 )
108 nfcv ⊢ Ⅎ 𝑙 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 )
109 100 fveq1d ⊢ ( 𝑙 = 𝑚 → ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
110 87 50 107 108 109 cbvmptf ⊢ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
111 110 eleq1i ⊢ ( ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ∈ dom ⇝ )
112 105 111 anbi12i ⊢ ( ( 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ∧ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) ) ∈ dom ⇝ ) ↔ ( 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ∈ dom ⇝ ) )
113 112 rabbia2 ⊢ { 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ∣ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) ) ∈ dom ⇝ } = { 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ∈ dom ⇝ }
114 99 113 eqtri ⊢ { 𝑦 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ∣ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ∈ dom ⇝ } = { 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ∈ dom ⇝ }
115 95 114 eqtri ⊢ 𝐷 = { 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ∈ dom ⇝ }
116 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ 𝐷 )
117 56 1 57 4 62 115 116 fnlimfvre ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) ∈ ℝ )
118 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
119 7 118 nfcxfr ⊢ Ⅎ 𝑥 𝐷
120 nfcv ⊢ Ⅎ 𝑦 𝐷
121 nfcv ⊢ Ⅎ 𝑦 ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
122 nfcv ⊢ Ⅎ 𝑥 ⇝
123 122 67 nffv ⊢ Ⅎ 𝑥 ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) )
124 70 fveq2d ⊢ ( 𝑥 = 𝑦 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) )
125 119 120 121 123 124 cbvmptf ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) )
126 8 125 eqtri ⊢ 𝐺 = ( 𝑦 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) )
127 117 126 fmptd ⊢ ( 𝜑 → 𝐺 : 𝐷 ⟶ ℝ )
128 3 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑀 ∈ ℤ )
129 5 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑆 ∈ SAlg )
130 6 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
131 nfcv ⊢ Ⅎ 𝑥 𝑙
132 2 131 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑙 )
133 132 65 nffv ⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 )
134 10 133 nfmpt ⊢ Ⅎ 𝑥 ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) )
135 122 134 nffv ⊢ Ⅎ 𝑥 ( ⇝ ‘ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) )
136 nfcv ⊢ Ⅎ 𝑙 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 )
137 nfcv ⊢ Ⅎ 𝑚 𝑥
138 75 137 nffv ⊢ Ⅎ 𝑚 ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 )
139 77 fveq1d ⊢ ( 𝑚 = 𝑙 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) )
140 50 87 136 138 139 cbvmptf ⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) )
141 140 a1i ⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) ) )
142 simpl ⊢ ( ( 𝑥 = 𝑦 ∧ 𝑙 ∈ 𝑍 ) → 𝑥 = 𝑦 )
143 142 fveq2d ⊢ ( ( 𝑥 = 𝑦 ∧ 𝑙 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) )
144 143 mpteq2dva ⊢ ( 𝑥 = 𝑦 → ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) ) = ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) )
145 141 144 eqtrd ⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) )
146 145 fveq2d ⊢ ( 𝑥 = 𝑦 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ) )
147 119 120 121 135 146 cbvmptf ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ) )
148 8 147 eqtri ⊢ 𝐺 = ( 𝑦 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ) )
149 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ )
150 nfcv ⊢ Ⅎ 𝑚 <
151 nfcv ⊢ Ⅎ 𝑚 ( 𝑎 + ( 1 / 𝑗 ) )
152 89 150 151 nfbr ⊢ Ⅎ 𝑚 ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) )
153 152 76 nfrabw ⊢ Ⅎ 𝑚 { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) }
154 nfcv ⊢ Ⅎ 𝑚 𝑡
155 154 76 nfin ⊢ Ⅎ 𝑚 ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) )
156 153 155 nfeq ⊢ Ⅎ 𝑚 { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) )
157 nfcv ⊢ Ⅎ 𝑚 𝑆
158 156 157 nfrabw ⊢ Ⅎ 𝑚 { 𝑡 ∈ 𝑆 ∣ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) }
159 nfcv ⊢ Ⅎ 𝑘 { 𝑡 ∈ 𝑆 ∣ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) }
160 nfcv ⊢ Ⅎ 𝑙 { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) }
161 nfcv ⊢ Ⅎ 𝑗 { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) }
162 nfcv ⊢ Ⅎ 𝑦 dom ( 𝐹 ‘ 𝑙 )
163 132 nfdm ⊢ Ⅎ 𝑥 dom ( 𝐹 ‘ 𝑙 )
164 nfcv ⊢ Ⅎ 𝑥 <
165 nfcv ⊢ Ⅎ 𝑥 ( 𝑎 + ( 1 / 𝑗 ) )
166 133 164 165 nfbr ⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) )
167 nfv ⊢ Ⅎ 𝑦 ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) )
168 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) )
169 168 breq1d ⊢ ( 𝑦 = 𝑥 → ( ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) ↔ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) ) )
170 162 163 166 167 169 cbvrabw ⊢ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = { 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) }
171 170 a1i ⊢ ( 𝑡 = 𝑠 → { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = { 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } )
172 ineq1 ⊢ ( 𝑡 = 𝑠 → ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑙 ) ) )
173 171 172 eqeq12d ⊢ ( 𝑡 = 𝑠 → ( { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) ↔ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑙 ) ) ) )
174 173 cbvrabv ⊢ { 𝑡 ∈ 𝑆 ∣ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑙 ) ) }
175 174 a1i ⊢ ( 𝑙 = 𝑚 → { 𝑡 ∈ 𝑆 ∣ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } )
176 101 eleq2d ⊢ ( 𝑙 = 𝑚 → ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ↔ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) )
177 100 fveq1d ⊢ ( 𝑙 = 𝑚 → ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
178 177 breq1d ⊢ ( 𝑙 = 𝑚 → ( ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) ↔ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) ) )
179 176 178 anbi12d ⊢ ( 𝑙 = 𝑚 → ( ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∧ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) ) ↔ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) ) ) )
180 179 rabbidva2 ⊢ ( 𝑙 = 𝑚 → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } )
181 101 ineq2d ⊢ ( 𝑙 = 𝑚 → ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑙 ) ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) )
182 180 181 eqeq12d ⊢ ( 𝑙 = 𝑚 → ( { 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑙 ) ) ↔ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
183 182 rabbidv ⊢ ( 𝑙 = 𝑚 → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
184 175 183 eqtrd ⊢ ( 𝑙 = 𝑚 → { 𝑡 ∈ 𝑆 ∣ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
185 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 1 / 𝑗 ) = ( 1 / 𝑘 ) )
186 185 oveq2d ⊢ ( 𝑗 = 𝑘 → ( 𝑎 + ( 1 / 𝑗 ) ) = ( 𝑎 + ( 1 / 𝑘 ) ) )
187 186 breq2d ⊢ ( 𝑗 = 𝑘 → ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) ↔ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) ) )
188 187 rabbidv ⊢ ( 𝑗 = 𝑘 → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) } )
189 188 eqeq1d ⊢ ( 𝑗 = 𝑘 → ( { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ↔ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
190 189 rabbidv ⊢ ( 𝑗 = 𝑘 → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
191 184 190 sylan9eq ⊢ ( ( 𝑙 = 𝑚 ∧ 𝑗 = 𝑘 ) → { 𝑡 ∈ 𝑆 ∣ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
192 158 159 160 161 191 cbvmpo ⊢ ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ { 𝑡 ∈ 𝑆 ∣ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } ) = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
193 192 eqcomi ⊢ ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) = ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ { 𝑡 ∈ 𝑆 ∣ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } )
194 128 4 129 130 95 148 149 193 smflimlem6 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑦 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑦 ) ≤ 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) )
195 9 5 44 127 194 issmfled ⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )