Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  smflim Structured version   Visualization version   GIF version

Theorem smflim 45480
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.)
Hypotheses
Ref Expression
smflim.n 𝑚𝐹
smflim.x 𝑥𝐹
smflim.m (𝜑𝑀 ∈ ℤ)
smflim.z 𝑍 = (ℤ𝑀)
smflim.s (𝜑𝑆 ∈ SAlg)
smflim.f (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
smflim.d 𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
smflim.g 𝐺 = (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
Assertion
Ref Expression
smflim (𝜑𝐺 ∈ (SMblFn‘𝑆))
Distinct variable groups:   𝑛,𝐹   𝑆,𝑚,𝑛   𝑚,𝑍,𝑥,𝑛   𝜑,𝑚,𝑛
Allowed substitution hints:   𝜑(𝑥)   𝐷(𝑥,𝑚,𝑛)   𝑆(𝑥)   𝐹(𝑥,𝑚)   𝐺(𝑥,𝑚,𝑛)   𝑀(𝑥,𝑚,𝑛)

Proof of Theorem smflim
Dummy variables 𝑖 𝑗 𝑙 𝑦 𝑘 𝑠 𝑡 𝑤 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1918 . 2 𝑎𝜑
2 smflim.s . 2 (𝜑𝑆 ∈ SAlg)
3 smflim.d . . . . 5 𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
4 nfcv 2904 . . . . . . 7 𝑥𝑍
5 nfcv 2904 . . . . . . . 8 𝑥(ℤ𝑛)
6 smflim.x . . . . . . . . . 10 𝑥𝐹
7 nfcv 2904 . . . . . . . . . 10 𝑥𝑚
86, 7nffv 6899 . . . . . . . . 9 𝑥(𝐹𝑚)
98nfdm 5949 . . . . . . . 8 𝑥dom (𝐹𝑚)
105, 9nfiin 5028 . . . . . . 7 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
114, 10nfiun 5027 . . . . . 6 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
1211ssrab2f 43792 . . . . 5 {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } ⊆ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
133, 12eqsstri 4016 . . . 4 𝐷 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
1413a1i 11 . . 3 (𝜑𝐷 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
15 uzssz 12840 . . . . . . . . 9 (ℤ𝑀) ⊆ ℤ
16 smflim.z . . . . . . . . . . 11 𝑍 = (ℤ𝑀)
1716eleq2i 2826 . . . . . . . . . 10 (𝑛𝑍𝑛 ∈ (ℤ𝑀))
1817biimpi 215 . . . . . . . . 9 (𝑛𝑍𝑛 ∈ (ℤ𝑀))
1915, 18sselid 3980 . . . . . . . 8 (𝑛𝑍𝑛 ∈ ℤ)
20 uzid 12834 . . . . . . . 8 (𝑛 ∈ ℤ → 𝑛 ∈ (ℤ𝑛))
2119, 20syl 17 . . . . . . 7 (𝑛𝑍𝑛 ∈ (ℤ𝑛))
2221adantl 483 . . . . . 6 ((𝜑𝑛𝑍) → 𝑛 ∈ (ℤ𝑛))
232adantr 482 . . . . . . 7 ((𝜑𝑛𝑍) → 𝑆 ∈ SAlg)
24 smflim.f . . . . . . . 8 (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
2524ffvelcdmda 7084 . . . . . . 7 ((𝜑𝑛𝑍) → (𝐹𝑛) ∈ (SMblFn‘𝑆))
26 eqid 2733 . . . . . . 7 dom (𝐹𝑛) = dom (𝐹𝑛)
2723, 25, 26smfdmss 45436 . . . . . 6 ((𝜑𝑛𝑍) → dom (𝐹𝑛) ⊆ 𝑆)
28 smflim.n . . . . . . . . . 10 𝑚𝐹
29 nfcv 2904 . . . . . . . . . 10 𝑚𝑛
3028, 29nffv 6899 . . . . . . . . 9 𝑚(𝐹𝑛)
3130nfdm 5949 . . . . . . . 8 𝑚dom (𝐹𝑛)
32 nfcv 2904 . . . . . . . 8 𝑚 𝑆
3331, 32nfss 3974 . . . . . . 7 𝑚dom (𝐹𝑛) ⊆ 𝑆
34 fveq2 6889 . . . . . . . . 9 (𝑚 = 𝑛 → (𝐹𝑚) = (𝐹𝑛))
3534dmeqd 5904 . . . . . . . 8 (𝑚 = 𝑛 → dom (𝐹𝑚) = dom (𝐹𝑛))
3635sseq1d 4013 . . . . . . 7 (𝑚 = 𝑛 → (dom (𝐹𝑚) ⊆ 𝑆 ↔ dom (𝐹𝑛) ⊆ 𝑆))
3733, 36rspce 3602 . . . . . 6 ((𝑛 ∈ (ℤ𝑛) ∧ dom (𝐹𝑛) ⊆ 𝑆) → ∃𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑆)
3822, 27, 37syl2anc 585 . . . . 5 ((𝜑𝑛𝑍) → ∃𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑆)
39 iinss 5059 . . . . 5 (∃𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑆 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑆)
4038, 39syl 17 . . . 4 ((𝜑𝑛𝑍) → 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑆)
4140iunssd 5053 . . 3 (𝜑 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑆)
4214, 41sstrd 3992 . 2 (𝜑𝐷 𝑆)
43 nfv 1918 . . . . 5 𝑚𝜑
44 nfcv 2904 . . . . . 6 𝑚𝑦
45 nfmpt1 5256 . . . . . . . . 9 𝑚(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))
46 nfcv 2904 . . . . . . . . 9 𝑚dom ⇝
4745, 46nfel 2918 . . . . . . . 8 𝑚(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝
48 nfcv 2904 . . . . . . . . 9 𝑚𝑍
49 nfii1 5032 . . . . . . . . 9 𝑚 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
5048, 49nfiun 5027 . . . . . . . 8 𝑚 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
5147, 50nfrabw 3469 . . . . . . 7 𝑚{𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
523, 51nfcxfr 2902 . . . . . 6 𝑚𝐷
5344, 52nfel 2918 . . . . 5 𝑚 𝑦𝐷
5443, 53nfan 1903 . . . 4 𝑚(𝜑𝑦𝐷)
55 nfcv 2904 . . . 4 𝑤𝐹
562adantr 482 . . . . . 6 ((𝜑𝑚𝑍) → 𝑆 ∈ SAlg)
5724ffvelcdmda 7084 . . . . . 6 ((𝜑𝑚𝑍) → (𝐹𝑚) ∈ (SMblFn‘𝑆))
58 eqid 2733 . . . . . 6 dom (𝐹𝑚) = dom (𝐹𝑚)
5956, 57, 58smff 45435 . . . . 5 ((𝜑𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
6059adantlr 714 . . . 4 (((𝜑𝑦𝐷) ∧ 𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
61 nfcv 2904 . . . . . . 7 𝑦 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
62 nfv 1918 . . . . . . 7 𝑦(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝
63 nfcv 2904 . . . . . . . . . 10 𝑥𝑦
648, 63nffv 6899 . . . . . . . . 9 𝑥((𝐹𝑚)‘𝑦)
654, 64nfmpt 5255 . . . . . . . 8 𝑥(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦))
6665nfel1 2920 . . . . . . 7 𝑥(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)) ∈ dom ⇝
67 fveq2 6889 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝐹𝑚)‘𝑥) = ((𝐹𝑚)‘𝑦))
6867mpteq2dv 5250 . . . . . . . 8 (𝑥 = 𝑦 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)))
6968eleq1d 2819 . . . . . . 7 (𝑥 = 𝑦 → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)) ∈ dom ⇝ ))
7011, 61, 62, 66, 69cbvrabw 3468 . . . . . 6 {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } = {𝑦 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)) ∈ dom ⇝ }
71 nfcv 2904 . . . . . . . . . . . . 13 𝑙dom (𝐹𝑚)
72 nfcv 2904 . . . . . . . . . . . . . . 15 𝑚𝑙
7328, 72nffv 6899 . . . . . . . . . . . . . 14 𝑚(𝐹𝑙)
7473nfdm 5949 . . . . . . . . . . . . 13 𝑚dom (𝐹𝑙)
75 fveq2 6889 . . . . . . . . . . . . . 14 (𝑚 = 𝑙 → (𝐹𝑚) = (𝐹𝑙))
7675dmeqd 5904 . . . . . . . . . . . . 13 (𝑚 = 𝑙 → dom (𝐹𝑚) = dom (𝐹𝑙))
7771, 74, 76cbviin 5040 . . . . . . . . . . . 12 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙)
7877a1i 11 . . . . . . . . . . 11 (𝑛 = 𝑖 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙))
79 fveq2 6889 . . . . . . . . . . . 12 (𝑛 = 𝑖 → (ℤ𝑛) = (ℤ𝑖))
80 eqidd 2734 . . . . . . . . . . . 12 ((𝑛 = 𝑖𝑙 ∈ (ℤ𝑖)) → dom (𝐹𝑙) = dom (𝐹𝑙))
8179, 80iineq12dv 43781 . . . . . . . . . . 11 (𝑛 = 𝑖 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙) = 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙))
8278, 81eqtrd 2773 . . . . . . . . . 10 (𝑛 = 𝑖 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙))
8382cbviunv 5043 . . . . . . . . 9 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙)
8483eleq2i 2826 . . . . . . . 8 (𝑦 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ↔ 𝑦 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙))
85 nfcv 2904 . . . . . . . . . 10 𝑙𝑍
86 nfcv 2904 . . . . . . . . . 10 𝑙((𝐹𝑚)‘𝑦)
8773, 44nffv 6899 . . . . . . . . . 10 𝑚((𝐹𝑙)‘𝑦)
8875fveq1d 6891 . . . . . . . . . 10 (𝑚 = 𝑙 → ((𝐹𝑚)‘𝑦) = ((𝐹𝑙)‘𝑦))
8948, 85, 86, 87, 88cbvmptf 5257 . . . . . . . . 9 (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)) = (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦))
9089eleq1i 2825 . . . . . . . 8 ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)) ∈ dom ⇝ ↔ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)) ∈ dom ⇝ )
9184, 90anbi12i 628 . . . . . . 7 ((𝑦 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)) ∈ dom ⇝ ) ↔ (𝑦 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ∧ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)) ∈ dom ⇝ ))
9291rabbia2 3436 . . . . . 6 {𝑦 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)) ∈ dom ⇝ } = {𝑦 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ∣ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)) ∈ dom ⇝ }
933, 70, 923eqtri 2765 . . . . 5 𝐷 = {𝑦 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ∣ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)) ∈ dom ⇝ }
94 fveq2 6889 . . . . . . . . 9 (𝑦 = 𝑤 → ((𝐹𝑙)‘𝑦) = ((𝐹𝑙)‘𝑤))
9594mpteq2dv 5250 . . . . . . . 8 (𝑦 = 𝑤 → (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)) = (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑤)))
9695eleq1d 2819 . . . . . . 7 (𝑦 = 𝑤 → ((𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)) ∈ dom ⇝ ↔ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑤)) ∈ dom ⇝ ))
9796cbvrabv 3443 . . . . . 6 {𝑦 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ∣ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)) ∈ dom ⇝ } = {𝑤 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ∣ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑤)) ∈ dom ⇝ }
98 fveq2 6889 . . . . . . . . . . . . 13 (𝑙 = 𝑚 → (𝐹𝑙) = (𝐹𝑚))
9998dmeqd 5904 . . . . . . . . . . . 12 (𝑙 = 𝑚 → dom (𝐹𝑙) = dom (𝐹𝑚))
10074, 71, 99cbviin 5040 . . . . . . . . . . 11 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) = 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)
101100a1i 11 . . . . . . . . . 10 (𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) = 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
102101iuneq2i 5018 . . . . . . . . 9 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) = 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)
103102eleq2i 2826 . . . . . . . 8 (𝑤 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ↔ 𝑤 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
104 nfcv 2904 . . . . . . . . . . 11 𝑚𝑤
10573, 104nffv 6899 . . . . . . . . . 10 𝑚((𝐹𝑙)‘𝑤)
106 nfcv 2904 . . . . . . . . . 10 𝑙((𝐹𝑚)‘𝑤)
10798fveq1d 6891 . . . . . . . . . 10 (𝑙 = 𝑚 → ((𝐹𝑙)‘𝑤) = ((𝐹𝑚)‘𝑤))
10885, 48, 105, 106, 107cbvmptf 5257 . . . . . . . . 9 (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑤)) = (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑤))
109108eleq1i 2825 . . . . . . . 8 ((𝑙𝑍 ↦ ((𝐹𝑙)‘𝑤)) ∈ dom ⇝ ↔ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑤)) ∈ dom ⇝ )
110103, 109anbi12i 628 . . . . . . 7 ((𝑤 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ∧ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑤)) ∈ dom ⇝ ) ↔ (𝑤 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚) ∧ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑤)) ∈ dom ⇝ ))
111110rabbia2 3436 . . . . . 6 {𝑤 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ∣ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑤)) ∈ dom ⇝ } = {𝑤 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑤)) ∈ dom ⇝ }
11297, 111eqtri 2761 . . . . 5 {𝑦 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ∣ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)) ∈ dom ⇝ } = {𝑤 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑤)) ∈ dom ⇝ }
11393, 112eqtri 2761 . . . 4 𝐷 = {𝑤 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑤)) ∈ dom ⇝ }
114 simpr 486 . . . 4 ((𝜑𝑦𝐷) → 𝑦𝐷)
11554, 28, 55, 16, 60, 113, 114fnlimfvre 44377 . . 3 ((𝜑𝑦𝐷) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦))) ∈ ℝ)
116 smflim.g . . . 4 𝐺 = (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
117 nfrab1 3452 . . . . . 6 𝑥{𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
1183, 117nfcxfr 2902 . . . . 5 𝑥𝐷
119 nfcv 2904 . . . . 5 𝑦𝐷
120 nfcv 2904 . . . . 5 𝑦( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)))
121 nfcv 2904 . . . . . 6 𝑥
122121, 65nffv 6899 . . . . 5 𝑥( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)))
12368fveq2d 6893 . . . . 5 (𝑥 = 𝑦 → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦))))
124118, 119, 120, 122, 123cbvmptf 5257 . . . 4 (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)))) = (𝑦𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦))))
125116, 124eqtri 2761 . . 3 𝐺 = (𝑦𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦))))
126115, 125fmptd 7111 . 2 (𝜑𝐺:𝐷⟶ℝ)
127 smflim.m . . . 4 (𝜑𝑀 ∈ ℤ)
128127adantr 482 . . 3 ((𝜑𝑎 ∈ ℝ) → 𝑀 ∈ ℤ)
1292adantr 482 . . 3 ((𝜑𝑎 ∈ ℝ) → 𝑆 ∈ SAlg)
13024adantr 482 . . 3 ((𝜑𝑎 ∈ ℝ) → 𝐹:𝑍⟶(SMblFn‘𝑆))
131 nfcv 2904 . . . . . . . . 9 𝑥𝑙
1326, 131nffv 6899 . . . . . . . 8 𝑥(𝐹𝑙)
133132, 63nffv 6899 . . . . . . 7 𝑥((𝐹𝑙)‘𝑦)
1344, 133nfmpt 5255 . . . . . 6 𝑥(𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦))
135121, 134nffv 6899 . . . . 5 𝑥( ⇝ ‘(𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)))
136 nfcv 2904 . . . . . . . . 9 𝑙((𝐹𝑚)‘𝑥)
137 nfcv 2904 . . . . . . . . . 10 𝑚𝑥
13873, 137nffv 6899 . . . . . . . . 9 𝑚((𝐹𝑙)‘𝑥)
13975fveq1d 6891 . . . . . . . . 9 (𝑚 = 𝑙 → ((𝐹𝑚)‘𝑥) = ((𝐹𝑙)‘𝑥))
14048, 85, 136, 138, 139cbvmptf 5257 . . . . . . . 8 (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑥))
141140a1i 11 . . . . . . 7 (𝑥 = 𝑦 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑥)))
142 simpl 484 . . . . . . . . 9 ((𝑥 = 𝑦𝑙𝑍) → 𝑥 = 𝑦)
143142fveq2d 6893 . . . . . . . 8 ((𝑥 = 𝑦𝑙𝑍) → ((𝐹𝑙)‘𝑥) = ((𝐹𝑙)‘𝑦))
144143mpteq2dva 5248 . . . . . . 7 (𝑥 = 𝑦 → (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑥)) = (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)))
145141, 144eqtrd 2773 . . . . . 6 (𝑥 = 𝑦 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)))
146145fveq2d 6893 . . . . 5 (𝑥 = 𝑦 → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = ( ⇝ ‘(𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦))))
147118, 119, 120, 135, 146cbvmptf 5257 . . . 4 (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)))) = (𝑦𝐷 ↦ ( ⇝ ‘(𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦))))
148116, 147eqtri 2761 . . 3 𝐺 = (𝑦𝐷 ↦ ( ⇝ ‘(𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦))))
149 simpr 486 . . 3 ((𝜑𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
150 nfcv 2904 . . . . . . . . 9 𝑚 <
151 nfcv 2904 . . . . . . . . 9 𝑚(𝑎 + (1 / 𝑗))
15287, 150, 151nfbr 5195 . . . . . . . 8 𝑚((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))
153152, 74nfrabw 3469 . . . . . . 7 𝑚{𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))}
154 nfcv 2904 . . . . . . . 8 𝑚𝑡
155154, 74nfin 4216 . . . . . . 7 𝑚(𝑡 ∩ dom (𝐹𝑙))
156153, 155nfeq 2917 . . . . . 6 𝑚{𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))
157 nfcv 2904 . . . . . 6 𝑚𝑆
158156, 157nfrabw 3469 . . . . 5 𝑚{𝑡𝑆 ∣ {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))}
159 nfcv 2904 . . . . 5 𝑘{𝑡𝑆 ∣ {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))}
160 nfcv 2904 . . . . 5 𝑙{𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))}
161 nfcv 2904 . . . . 5 𝑗{𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))}
162 nfcv 2904 . . . . . . . . . . . 12 𝑦dom (𝐹𝑙)
163132nfdm 5949 . . . . . . . . . . . 12 𝑥dom (𝐹𝑙)
164 nfcv 2904 . . . . . . . . . . . . 13 𝑥 <
165 nfcv 2904 . . . . . . . . . . . . 13 𝑥(𝑎 + (1 / 𝑗))
166133, 164, 165nfbr 5195 . . . . . . . . . . . 12 𝑥((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))
167 nfv 1918 . . . . . . . . . . . 12 𝑦((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))
168 fveq2 6889 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → ((𝐹𝑙)‘𝑦) = ((𝐹𝑙)‘𝑥))
169168breq1d 5158 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗)) ↔ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))))
170162, 163, 166, 167, 169cbvrabw 3468 . . . . . . . . . . 11 {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = {𝑥 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))}
171170a1i 11 . . . . . . . . . 10 (𝑡 = 𝑠 → {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = {𝑥 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))})
172 ineq1 4205 . . . . . . . . . 10 (𝑡 = 𝑠 → (𝑡 ∩ dom (𝐹𝑙)) = (𝑠 ∩ dom (𝐹𝑙)))
173171, 172eqeq12d 2749 . . . . . . . . 9 (𝑡 = 𝑠 → ({𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙)) ↔ {𝑥 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑙))))
174173cbvrabv 3443 . . . . . . . 8 {𝑡𝑆 ∣ {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))} = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑙))}
175174a1i 11 . . . . . . 7 (𝑙 = 𝑚 → {𝑡𝑆 ∣ {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))} = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑙))})
17699eleq2d 2820 . . . . . . . . . . 11 (𝑙 = 𝑚 → (𝑥 ∈ dom (𝐹𝑙) ↔ 𝑥 ∈ dom (𝐹𝑚)))
17798fveq1d 6891 . . . . . . . . . . . 12 (𝑙 = 𝑚 → ((𝐹𝑙)‘𝑥) = ((𝐹𝑚)‘𝑥))
178177breq1d 5158 . . . . . . . . . . 11 (𝑙 = 𝑚 → (((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗)) ↔ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))))
179176, 178anbi12d 632 . . . . . . . . . 10 (𝑙 = 𝑚 → ((𝑥 ∈ dom (𝐹𝑙) ∧ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))) ↔ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗)))))
180179rabbidva2 3435 . . . . . . . . 9 (𝑙 = 𝑚 → {𝑥 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))})
18199ineq2d 4212 . . . . . . . . 9 (𝑙 = 𝑚 → (𝑠 ∩ dom (𝐹𝑙)) = (𝑠 ∩ dom (𝐹𝑚)))
182180, 181eqeq12d 2749 . . . . . . . 8 (𝑙 = 𝑚 → ({𝑥 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑙)) ↔ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))))
183182rabbidv 3441 . . . . . . 7 (𝑙 = 𝑚 → {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑙))} = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))})
184175, 183eqtrd 2773 . . . . . 6 (𝑙 = 𝑚 → {𝑡𝑆 ∣ {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))} = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))})
185 oveq2 7414 . . . . . . . . . . 11 (𝑗 = 𝑘 → (1 / 𝑗) = (1 / 𝑘))
186185oveq2d 7422 . . . . . . . . . 10 (𝑗 = 𝑘 → (𝑎 + (1 / 𝑗)) = (𝑎 + (1 / 𝑘)))
187186breq2d 5160 . . . . . . . . 9 (𝑗 = 𝑘 → (((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗)) ↔ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))))
188187rabbidv 3441 . . . . . . . 8 (𝑗 = 𝑘 → {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))})
189188eqeq1d 2735 . . . . . . 7 (𝑗 = 𝑘 → ({𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚)) ↔ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))))
190189rabbidv 3441 . . . . . 6 (𝑗 = 𝑘 → {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))} = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))})
191184, 190sylan9eq 2793 . . . . 5 ((𝑙 = 𝑚𝑗 = 𝑘) → {𝑡𝑆 ∣ {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))} = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))})
192158, 159, 160, 161, 191cbvmpo 7500 . . . 4 (𝑙𝑍, 𝑗 ∈ ℕ ↦ {𝑡𝑆 ∣ {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))}) = (𝑚𝑍, 𝑘 ∈ ℕ ↦ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))})
193192eqcomi 2742 . . 3 (𝑚𝑍, 𝑘 ∈ ℕ ↦ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))}) = (𝑙𝑍, 𝑗 ∈ ℕ ↦ {𝑡𝑆 ∣ {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))})
194128, 16, 129, 130, 93, 148, 149, 193smflimlem6 45479 . 2 ((𝜑𝑎 ∈ ℝ) → {𝑦𝐷 ∣ (𝐺𝑦) ≤ 𝑎} ∈ (𝑆t 𝐷))
1951, 2, 42, 126, 194issmfled 45460 1 (𝜑𝐺 ∈ (SMblFn‘𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  wnfc 2884  wrex 3071  {crab 3433  cin 3947  wss 3948   cuni 4908   ciun 4997   ciin 4998   class class class wbr 5148  cmpt 5231  dom cdm 5676  wf 6537  cfv 6541  (class class class)co 7406  cmpo 7408  cr 11106  1c1 11108   + caddc 11110   < clt 11245   / cdiv 11868  cn 12209  cz 12555  cuz 12819  cli 15425  SAlgcsalg 45011  SMblFncsmblfn 45398
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-inf2 9633  ax-cc 10427  ax-ac2 10455  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-oadd 8467  df-omul 8468  df-er 8700  df-map 8819  df-pm 8820  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-sup 9434  df-inf 9435  df-oi 9502  df-card 9931  df-acn 9934  df-ac 10108  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-n0 12470  df-z 12556  df-uz 12820  df-q 12930  df-rp 12972  df-ioo 13325  df-ico 13327  df-fl 13754  df-seq 13964  df-exp 14025  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-clim 15429  df-rlim 15430  df-rest 17365  df-salg 45012  df-smblfn 45399
This theorem is referenced by:  smflim2  45509
  Copyright terms: Public domain W3C validator