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

Theorem smflim 41483
 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 1984 . 2 𝑎𝜑
2 smflim.s . 2 (𝜑𝑆 ∈ SAlg)
3 smflim.d . . . . 5 𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
4 nfcv 2894 . . . . . . 7 𝑥𝑍
5 nfcv 2894 . . . . . . . 8 𝑥(ℤ𝑛)
6 smflim.x . . . . . . . . . 10 𝑥𝐹
7 nfcv 2894 . . . . . . . . . 10 𝑥𝑚
86, 7nffv 6351 . . . . . . . . 9 𝑥(𝐹𝑚)
98nfdm 5514 . . . . . . . 8 𝑥dom (𝐹𝑚)
105, 9nfiin 4693 . . . . . . 7 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
114, 10nfiun 4692 . . . . . 6 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
1211ssrab2f 39791 . . . . 5 {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } ⊆ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
133, 12eqsstri 3768 . . . 4 𝐷 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
1413a1i 11 . . 3 (𝜑𝐷 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
15 uzssz 11891 . . . . . . . . 9 (ℤ𝑀) ⊆ ℤ
16 smflim.z . . . . . . . . . . 11 𝑍 = (ℤ𝑀)
1716eleq2i 2823 . . . . . . . . . 10 (𝑛𝑍𝑛 ∈ (ℤ𝑀))
1817biimpi 206 . . . . . . . . 9 (𝑛𝑍𝑛 ∈ (ℤ𝑀))
1915, 18sseldi 3734 . . . . . . . 8 (𝑛𝑍𝑛 ∈ ℤ)
20 uzid 11886 . . . . . . . 8 (𝑛 ∈ ℤ → 𝑛 ∈ (ℤ𝑛))
2119, 20syl 17 . . . . . . 7 (𝑛𝑍𝑛 ∈ (ℤ𝑛))
2221adantl 473 . . . . . 6 ((𝜑𝑛𝑍) → 𝑛 ∈ (ℤ𝑛))
232adantr 472 . . . . . . 7 ((𝜑𝑛𝑍) → 𝑆 ∈ SAlg)
24 smflim.f . . . . . . . 8 (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
2524ffvelrnda 6514 . . . . . . 7 ((𝜑𝑛𝑍) → (𝐹𝑛) ∈ (SMblFn‘𝑆))
26 eqid 2752 . . . . . . 7 dom (𝐹𝑛) = dom (𝐹𝑛)
2723, 25, 26smfdmss 41440 . . . . . 6 ((𝜑𝑛𝑍) → dom (𝐹𝑛) ⊆ 𝑆)
28 smflim.n . . . . . . . . . 10 𝑚𝐹
29 nfcv 2894 . . . . . . . . . 10 𝑚𝑛
3028, 29nffv 6351 . . . . . . . . 9 𝑚(𝐹𝑛)
3130nfdm 5514 . . . . . . . 8 𝑚dom (𝐹𝑛)
32 nfcv 2894 . . . . . . . 8 𝑚 𝑆
3331, 32nfss 3729 . . . . . . 7 𝑚dom (𝐹𝑛) ⊆ 𝑆
34 fveq2 6344 . . . . . . . . 9 (𝑚 = 𝑛 → (𝐹𝑚) = (𝐹𝑛))
3534dmeqd 5473 . . . . . . . 8 (𝑚 = 𝑛 → dom (𝐹𝑚) = dom (𝐹𝑛))
3635sseq1d 3765 . . . . . . 7 (𝑚 = 𝑛 → (dom (𝐹𝑚) ⊆ 𝑆 ↔ dom (𝐹𝑛) ⊆ 𝑆))
3733, 36rspce 3436 . . . . . 6 ((𝑛 ∈ (ℤ𝑛) ∧ dom (𝐹𝑛) ⊆ 𝑆) → ∃𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑆)
3822, 27, 37syl2anc 696 . . . . 5 ((𝜑𝑛𝑍) → ∃𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑆)
39 iinss 4715 . . . . 5 (∃𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑆 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑆)
4038, 39syl 17 . . . 4 ((𝜑𝑛𝑍) → 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑆)
4140iunssd 39762 . . 3 (𝜑 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑆)
4214, 41sstrd 3746 . 2 (𝜑𝐷 𝑆)
43 nfv 1984 . . . . 5 𝑚𝜑
44 nfcv 2894 . . . . . 6 𝑚𝑦
45 nfmpt1 4891 . . . . . . . . 9 𝑚(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))
46 nfcv 2894 . . . . . . . . 9 𝑚dom ⇝
4745, 46nfel 2907 . . . . . . . 8 𝑚(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝
48 nfcv 2894 . . . . . . . . 9 𝑚𝑍
49 nfii1 4695 . . . . . . . . 9 𝑚 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
5048, 49nfiun 4692 . . . . . . . 8 𝑚 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
5147, 50nfrab 3254 . . . . . . 7 𝑚{𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
523, 51nfcxfr 2892 . . . . . 6 𝑚𝐷
5344, 52nfel 2907 . . . . 5 𝑚 𝑦𝐷
5443, 53nfan 1969 . . . 4 𝑚(𝜑𝑦𝐷)
55 nfcv 2894 . . . 4 𝑤𝐹
562adantr 472 . . . . . 6 ((𝜑𝑚𝑍) → 𝑆 ∈ SAlg)
5724ffvelrnda 6514 . . . . . 6 ((𝜑𝑚𝑍) → (𝐹𝑚) ∈ (SMblFn‘𝑆))
58 eqid 2752 . . . . . 6 dom (𝐹𝑚) = dom (𝐹𝑚)
5956, 57, 58smff 41439 . . . . 5 ((𝜑𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
6059adantlr 753 . . . 4 (((𝜑𝑦𝐷) ∧ 𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
61 nfcv 2894 . . . . . . 7 𝑦 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
62 nfv 1984 . . . . . . 7 𝑦(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝
63 nfcv 2894 . . . . . . . . . 10 𝑥𝑦
648, 63nffv 6351 . . . . . . . . 9 𝑥((𝐹𝑚)‘𝑦)
654, 64nfmpt 4890 . . . . . . . 8 𝑥(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦))
6665nfel1 2909 . . . . . . 7 𝑥(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)) ∈ dom ⇝
67 fveq2 6344 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝐹𝑚)‘𝑥) = ((𝐹𝑚)‘𝑦))
6867mpteq2dv 4889 . . . . . . . 8 (𝑥 = 𝑦 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)))
6968eleq1d 2816 . . . . . . 7 (𝑥 = 𝑦 → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)) ∈ dom ⇝ ))
7011, 61, 62, 66, 69cbvrab 3330 . . . . . 6 {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } = {𝑦 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)) ∈ dom ⇝ }
71 nfcv 2894 . . . . . . . . . . . . 13 𝑙dom (𝐹𝑚)
72 nfcv 2894 . . . . . . . . . . . . . . 15 𝑚𝑙
7328, 72nffv 6351 . . . . . . . . . . . . . 14 𝑚(𝐹𝑙)
7473nfdm 5514 . . . . . . . . . . . . 13 𝑚dom (𝐹𝑙)
75 fveq2 6344 . . . . . . . . . . . . . 14 (𝑚 = 𝑙 → (𝐹𝑚) = (𝐹𝑙))
7675dmeqd 5473 . . . . . . . . . . . . 13 (𝑚 = 𝑙 → dom (𝐹𝑚) = dom (𝐹𝑙))
7771, 74, 76cbviin 4702 . . . . . . . . . . . 12 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙)
7877a1i 11 . . . . . . . . . . 11 (𝑛 = 𝑖 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙))
79 fveq2 6344 . . . . . . . . . . . 12 (𝑛 = 𝑖 → (ℤ𝑛) = (ℤ𝑖))
80 eqidd 2753 . . . . . . . . . . . 12 ((𝑛 = 𝑖𝑙 ∈ (ℤ𝑖)) → dom (𝐹𝑙) = dom (𝐹𝑙))
8179, 80iineq12dv 39780 . . . . . . . . . . 11 (𝑛 = 𝑖 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙) = 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙))
8278, 81eqtrd 2786 . . . . . . . . . 10 (𝑛 = 𝑖 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙))
8382cbviunv 4703 . . . . . . . . 9 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙)
8483eleq2i 2823 . . . . . . . 8 (𝑦 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ↔ 𝑦 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙))
85 nfcv 2894 . . . . . . . . . 10 𝑙𝑍
86 nfcv 2894 . . . . . . . . . 10 𝑙((𝐹𝑚)‘𝑦)
8773, 44nffv 6351 . . . . . . . . . 10 𝑚((𝐹𝑙)‘𝑦)
8875fveq1d 6346 . . . . . . . . . 10 (𝑚 = 𝑙 → ((𝐹𝑚)‘𝑦) = ((𝐹𝑙)‘𝑦))
8948, 85, 86, 87, 88cbvmptf 4892 . . . . . . . . 9 (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)) = (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦))
9089eleq1i 2822 . . . . . . . 8 ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)) ∈ dom ⇝ ↔ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)) ∈ dom ⇝ )
9184, 90anbi12i 735 . . . . . . 7 ((𝑦 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)) ∈ dom ⇝ ) ↔ (𝑦 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ∧ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)) ∈ dom ⇝ ))
9291rabbia2 3319 . . . . . 6 {𝑦 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)) ∈ dom ⇝ } = {𝑦 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ∣ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)) ∈ dom ⇝ }
933, 70, 923eqtri 2778 . . . . 5 𝐷 = {𝑦 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ∣ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)) ∈ dom ⇝ }
94 fveq2 6344 . . . . . . . . 9 (𝑦 = 𝑤 → ((𝐹𝑙)‘𝑦) = ((𝐹𝑙)‘𝑤))
9594mpteq2dv 4889 . . . . . . . 8 (𝑦 = 𝑤 → (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)) = (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑤)))
9695eleq1d 2816 . . . . . . 7 (𝑦 = 𝑤 → ((𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)) ∈ dom ⇝ ↔ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑤)) ∈ dom ⇝ ))
9796cbvrabv 3331 . . . . . 6 {𝑦 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ∣ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)) ∈ dom ⇝ } = {𝑤 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ∣ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑤)) ∈ dom ⇝ }
98 fveq2 6344 . . . . . . . . . . . . 13 (𝑙 = 𝑚 → (𝐹𝑙) = (𝐹𝑚))
9998dmeqd 5473 . . . . . . . . . . . 12 (𝑙 = 𝑚 → dom (𝐹𝑙) = dom (𝐹𝑚))
10074, 71, 99cbviin 4702 . . . . . . . . . . 11 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) = 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)
101100a1i 11 . . . . . . . . . 10 (𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) = 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
102101iuneq2i 4683 . . . . . . . . 9 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) = 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)
103102eleq2i 2823 . . . . . . . 8 (𝑤 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ↔ 𝑤 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
104 nfcv 2894 . . . . . . . . . . 11 𝑚𝑤
10573, 104nffv 6351 . . . . . . . . . 10 𝑚((𝐹𝑙)‘𝑤)
106 nfcv 2894 . . . . . . . . . 10 𝑙((𝐹𝑚)‘𝑤)
10798fveq1d 6346 . . . . . . . . . 10 (𝑙 = 𝑚 → ((𝐹𝑙)‘𝑤) = ((𝐹𝑚)‘𝑤))
10885, 48, 105, 106, 107cbvmptf 4892 . . . . . . . . 9 (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑤)) = (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑤))
109108eleq1i 2822 . . . . . . . 8 ((𝑙𝑍 ↦ ((𝐹𝑙)‘𝑤)) ∈ dom ⇝ ↔ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑤)) ∈ dom ⇝ )
110103, 109anbi12i 735 . . . . . . 7 ((𝑤 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ∧ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑤)) ∈ dom ⇝ ) ↔ (𝑤 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚) ∧ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑤)) ∈ dom ⇝ ))
111110rabbia2 3319 . . . . . 6 {𝑤 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ∣ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑤)) ∈ dom ⇝ } = {𝑤 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑤)) ∈ dom ⇝ }
11297, 111eqtri 2774 . . . . 5 {𝑦 𝑖𝑍 𝑙 ∈ (ℤ𝑖)dom (𝐹𝑙) ∣ (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)) ∈ dom ⇝ } = {𝑤 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑤)) ∈ dom ⇝ }
11393, 112eqtri 2774 . . . 4 𝐷 = {𝑤 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑤)) ∈ dom ⇝ }
114 simpr 479 . . . 4 ((𝜑𝑦𝐷) → 𝑦𝐷)
11554, 28, 55, 16, 60, 113, 114fnlimfvre 40401 . . 3 ((𝜑𝑦𝐷) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦))) ∈ ℝ)
116 smflim.g . . . 4 𝐺 = (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
117 nfrab1 3253 . . . . . 6 𝑥{𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
1183, 117nfcxfr 2892 . . . . 5 𝑥𝐷
119 nfcv 2894 . . . . 5 𝑦𝐷
120 nfcv 2894 . . . . 5 𝑦( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)))
121 nfcv 2894 . . . . . 6 𝑥
122121, 65nffv 6351 . . . . 5 𝑥( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦)))
12368fveq2d 6348 . . . . 5 (𝑥 = 𝑦 → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦))))
124118, 119, 120, 122, 123cbvmptf 4892 . . . 4 (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)))) = (𝑦𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦))))
125116, 124eqtri 2774 . . 3 𝐺 = (𝑦𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑦))))
126115, 125fmptd 6540 . 2 (𝜑𝐺:𝐷⟶ℝ)
127 smflim.m . . . 4 (𝜑𝑀 ∈ ℤ)
128127adantr 472 . . 3 ((𝜑𝑎 ∈ ℝ) → 𝑀 ∈ ℤ)
1292adantr 472 . . 3 ((𝜑𝑎 ∈ ℝ) → 𝑆 ∈ SAlg)
13024adantr 472 . . 3 ((𝜑𝑎 ∈ ℝ) → 𝐹:𝑍⟶(SMblFn‘𝑆))
131 nfcv 2894 . . . . . . . . 9 𝑥𝑙
1326, 131nffv 6351 . . . . . . . 8 𝑥(𝐹𝑙)
133132, 63nffv 6351 . . . . . . 7 𝑥((𝐹𝑙)‘𝑦)
1344, 133nfmpt 4890 . . . . . 6 𝑥(𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦))
135121, 134nffv 6351 . . . . 5 𝑥( ⇝ ‘(𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)))
136 nfcv 2894 . . . . . . . . 9 𝑙((𝐹𝑚)‘𝑥)
137 nfcv 2894 . . . . . . . . . 10 𝑚𝑥
13873, 137nffv 6351 . . . . . . . . 9 𝑚((𝐹𝑙)‘𝑥)
13975fveq1d 6346 . . . . . . . . 9 (𝑚 = 𝑙 → ((𝐹𝑚)‘𝑥) = ((𝐹𝑙)‘𝑥))
14048, 85, 136, 138, 139cbvmptf 4892 . . . . . . . 8 (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑥))
141140a1i 11 . . . . . . 7 (𝑥 = 𝑦 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑥)))
142 simpl 474 . . . . . . . . 9 ((𝑥 = 𝑦𝑙𝑍) → 𝑥 = 𝑦)
143142fveq2d 6348 . . . . . . . 8 ((𝑥 = 𝑦𝑙𝑍) → ((𝐹𝑙)‘𝑥) = ((𝐹𝑙)‘𝑦))
144143mpteq2dva 4888 . . . . . . 7 (𝑥 = 𝑦 → (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑥)) = (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)))
145141, 144eqtrd 2786 . . . . . 6 (𝑥 = 𝑦 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦)))
146145fveq2d 6348 . . . . 5 (𝑥 = 𝑦 → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = ( ⇝ ‘(𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦))))
147118, 119, 120, 135, 146cbvmptf 4892 . . . 4 (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)))) = (𝑦𝐷 ↦ ( ⇝ ‘(𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦))))
148116, 147eqtri 2774 . . 3 𝐺 = (𝑦𝐷 ↦ ( ⇝ ‘(𝑙𝑍 ↦ ((𝐹𝑙)‘𝑦))))
149 simpr 479 . . 3 ((𝜑𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
150 nfcv 2894 . . . . . . . . 9 𝑚 <
151 nfcv 2894 . . . . . . . . 9 𝑚(𝑎 + (1 / 𝑗))
15287, 150, 151nfbr 4843 . . . . . . . 8 𝑚((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))
153152, 74nfrab 3254 . . . . . . 7 𝑚{𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))}
154 nfcv 2894 . . . . . . . 8 𝑚𝑡
155154, 74nfin 3955 . . . . . . 7 𝑚(𝑡 ∩ dom (𝐹𝑙))
156153, 155nfeq 2906 . . . . . 6 𝑚{𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))
157 nfcv 2894 . . . . . 6 𝑚𝑆
158156, 157nfrab 3254 . . . . 5 𝑚{𝑡𝑆 ∣ {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))}
159 nfcv 2894 . . . . 5 𝑘{𝑡𝑆 ∣ {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))}
160 nfcv 2894 . . . . 5 𝑙{𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))}
161 nfcv 2894 . . . . 5 𝑗{𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))}
162 nfcv 2894 . . . . . . . . . . . 12 𝑦dom (𝐹𝑙)
163132nfdm 5514 . . . . . . . . . . . 12 𝑥dom (𝐹𝑙)
164 nfcv 2894 . . . . . . . . . . . . 13 𝑥 <
165 nfcv 2894 . . . . . . . . . . . . 13 𝑥(𝑎 + (1 / 𝑗))
166133, 164, 165nfbr 4843 . . . . . . . . . . . 12 𝑥((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))
167 nfv 1984 . . . . . . . . . . . 12 𝑦((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))
168 fveq2 6344 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → ((𝐹𝑙)‘𝑦) = ((𝐹𝑙)‘𝑥))
169168breq1d 4806 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗)) ↔ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))))
170162, 163, 166, 167, 169cbvrab 3330 . . . . . . . . . . 11 {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = {𝑥 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))}
171170a1i 11 . . . . . . . . . 10 (𝑡 = 𝑠 → {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = {𝑥 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))})
172 ineq1 3942 . . . . . . . . . 10 (𝑡 = 𝑠 → (𝑡 ∩ dom (𝐹𝑙)) = (𝑠 ∩ dom (𝐹𝑙)))
173171, 172eqeq12d 2767 . . . . . . . . 9 (𝑡 = 𝑠 → ({𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙)) ↔ {𝑥 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑙))))
174173cbvrabv 3331 . . . . . . . 8 {𝑡𝑆 ∣ {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))} = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑙))}
175174a1i 11 . . . . . . 7 (𝑙 = 𝑚 → {𝑡𝑆 ∣ {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))} = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑙))})
17699eleq2d 2817 . . . . . . . . . . 11 (𝑙 = 𝑚 → (𝑥 ∈ dom (𝐹𝑙) ↔ 𝑥 ∈ dom (𝐹𝑚)))
17798fveq1d 6346 . . . . . . . . . . . 12 (𝑙 = 𝑚 → ((𝐹𝑙)‘𝑥) = ((𝐹𝑚)‘𝑥))
178177breq1d 4806 . . . . . . . . . . 11 (𝑙 = 𝑚 → (((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗)) ↔ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))))
179176, 178anbi12d 749 . . . . . . . . . 10 (𝑙 = 𝑚 → ((𝑥 ∈ dom (𝐹𝑙) ∧ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))) ↔ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗)))))
180179rabbidva2 3318 . . . . . . . . 9 (𝑙 = 𝑚 → {𝑥 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))})
18199ineq2d 3949 . . . . . . . . 9 (𝑙 = 𝑚 → (𝑠 ∩ dom (𝐹𝑙)) = (𝑠 ∩ dom (𝐹𝑚)))
182180, 181eqeq12d 2767 . . . . . . . 8 (𝑙 = 𝑚 → ({𝑥 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑙)) ↔ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))))
183182rabbidv 3321 . . . . . . 7 (𝑙 = 𝑚 → {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑙))} = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))})
184175, 183eqtrd 2786 . . . . . 6 (𝑙 = 𝑚 → {𝑡𝑆 ∣ {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))} = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))})
185 oveq2 6813 . . . . . . . . . . 11 (𝑗 = 𝑘 → (1 / 𝑗) = (1 / 𝑘))
186185oveq2d 6821 . . . . . . . . . 10 (𝑗 = 𝑘 → (𝑎 + (1 / 𝑗)) = (𝑎 + (1 / 𝑘)))
187186breq2d 4808 . . . . . . . . 9 (𝑗 = 𝑘 → (((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗)) ↔ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))))
188187rabbidv 3321 . . . . . . . 8 (𝑗 = 𝑘 → {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))})
189188eqeq1d 2754 . . . . . . 7 (𝑗 = 𝑘 → ({𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚)) ↔ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))))
190189rabbidv 3321 . . . . . 6 (𝑗 = 𝑘 → {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))} = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))})
191184, 190sylan9eq 2806 . . . . 5 ((𝑙 = 𝑚𝑗 = 𝑘) → {𝑡𝑆 ∣ {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))} = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))})
192158, 159, 160, 161, 191cbvmpt2 6891 . . . 4 (𝑙𝑍, 𝑗 ∈ ℕ ↦ {𝑡𝑆 ∣ {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))}) = (𝑚𝑍, 𝑘 ∈ ℕ ↦ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))})
193192eqcomi 2761 . . 3 (𝑚𝑍, 𝑘 ∈ ℕ ↦ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))}) = (𝑙𝑍, 𝑗 ∈ ℕ ↦ {𝑡𝑆 ∣ {𝑦 ∈ dom (𝐹𝑙) ∣ ((𝐹𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹𝑙))})
194128, 16, 129, 130, 93, 148, 149, 193smflimlem6 41482 . 2 ((𝜑𝑎 ∈ ℝ) → {𝑦𝐷 ∣ (𝐺𝑦) ≤ 𝑎} ∈ (𝑆t 𝐷))
1951, 2, 42, 126, 194issmfled 41464 1 (𝜑𝐺 ∈ (SMblFn‘𝑆))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1624   ∈ wcel 2131  Ⅎwnfc 2881  ∃wrex 3043  {crab 3046   ∩ cin 3706   ⊆ wss 3707  ∪ cuni 4580  ∪ ciun 4664  ∩ ciin 4665   class class class wbr 4796   ↦ cmpt 4873  dom cdm 5258  ⟶wf 6037  ‘cfv 6041  (class class class)co 6805   ↦ cmpt2 6807  ℝcr 10119  1c1 10121   + caddc 10123   < clt 10258   / cdiv 10868  ℕcn 11204  ℤcz 11561  ℤ≥cuz 11871   ⇝ cli 14406  SAlgcsalg 41023  SMblFncsmblfn 41407 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-inf2 8703  ax-cc 9441  ax-ac2 9469  ax-cnex 10176  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-mulcom 10184  ax-addass 10185  ax-mulass 10186  ax-distr 10187  ax-i2m1 10188  ax-1ne0 10189  ax-1rid 10190  ax-rnegex 10191  ax-rrecex 10192  ax-cnre 10193  ax-pre-lttri 10194  ax-pre-lttrn 10195  ax-pre-ltadd 10196  ax-pre-mulgt0 10197  ax-pre-sup 10198 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-int 4620  df-iun 4666  df-iin 4667  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-se 5218  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-isom 6050  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-om 7223  df-1st 7325  df-2nd 7326  df-wrecs 7568  df-recs 7629  df-rdg 7667  df-1o 7721  df-oadd 7725  df-omul 7726  df-er 7903  df-map 8017  df-pm 8018  df-en 8114  df-dom 8115  df-sdom 8116  df-fin 8117  df-sup 8505  df-inf 8506  df-oi 8572  df-card 8947  df-acn 8950  df-ac 9121  df-pnf 10260  df-mnf 10261  df-xr 10262  df-ltxr 10263  df-le 10264  df-sub 10452  df-neg 10453  df-div 10869  df-nn 11205  df-2 11263  df-3 11264  df-n0 11477  df-z 11562  df-uz 11872  df-q 11974  df-rp 12018  df-ioo 12364  df-ico 12366  df-fl 12779  df-seq 12988  df-exp 13047  df-cj 14030  df-re 14031  df-im 14032  df-sqrt 14166  df-abs 14167  df-clim 14410  df-rlim 14411  df-rest 16277  df-salg 41024  df-smblfn 41408 This theorem is referenced by:  smflim2  41510
 Copyright terms: Public domain W3C validator