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

Theorem smflimmpt 41337
 Description: The limit of a sequence 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 ). 𝐴 can contain 𝑚 as a free variable, in other words it can be thought as an indexed collection 𝐴(𝑚). 𝐵 can be thought as a collection with two indexes 𝐵(𝑚, 𝑥). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
Hypotheses
Ref Expression
smflimmpt.p 𝑚𝜑
smflimmpt.x 𝑥𝜑
smflimmpt.n 𝑛𝜑
smflimmpt.m (𝜑𝑀 ∈ ℤ)
smflimmpt.z 𝑍 = (ℤ𝑀)
smflimmpt.a ((𝜑𝑚𝑍) → 𝐴𝑉)
smflimmpt.b ((𝜑𝑚𝑍𝑥𝐴) → 𝐵𝑊)
smflimmpt.s (𝜑𝑆 ∈ SAlg)
smflimmpt.l ((𝜑𝑚𝑍) → (𝑥𝐴𝐵) ∈ (SMblFn‘𝑆))
smflimmpt.d 𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (𝑚𝑍𝐵) ∈ dom ⇝ }
smflimmpt.g 𝐺 = (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍𝐵)))
Assertion
Ref Expression
smflimmpt (𝜑𝐺 ∈ (SMblFn‘𝑆))
Distinct variable groups:   𝐴,𝑛,𝑥   𝐵,𝑛   𝑆,𝑚,𝑛   𝑚,𝑍,𝑛,𝑥
Allowed substitution hints:   𝜑(𝑥,𝑚,𝑛)   𝐴(𝑚)   𝐵(𝑥,𝑚)   𝐷(𝑥,𝑚,𝑛)   𝑆(𝑥)   𝐺(𝑥,𝑚,𝑛)   𝑀(𝑥,𝑚,𝑛)   𝑉(𝑥,𝑚,𝑛)   𝑊(𝑥,𝑚,𝑛)

Proof of Theorem smflimmpt
StepHypRef Expression
1 smflimmpt.g . . . 4 𝐺 = (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍𝐵)))
21a1i 11 . . 3 (𝜑𝐺 = (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍𝐵))))
3 smflimmpt.x . . . 4 𝑥𝜑
4 smflimmpt.d . . . . . 6 𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (𝑚𝑍𝐵) ∈ dom ⇝ }
54a1i 11 . . . . 5 (𝜑𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (𝑚𝑍𝐵) ∈ dom ⇝ })
6 smflimmpt.n . . . . . . . . . . . . . 14 𝑛𝜑
7 smflimmpt.p . . . . . . . . . . . . . . . 16 𝑚𝜑
8 nfv 1883 . . . . . . . . . . . . . . . 16 𝑚 𝑛𝑍
97, 8nfan 1868 . . . . . . . . . . . . . . 15 𝑚(𝜑𝑛𝑍)
10 smflimmpt.z . . . . . . . . . . . . . . . . . . . 20 𝑍 = (ℤ𝑀)
1110uztrn2 11743 . . . . . . . . . . . . . . . . . . 19 ((𝑛𝑍𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
1211adantll 750 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
13 simpll 805 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝜑)
14 smflimmpt.a . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚𝑍) → 𝐴𝑉)
1514mptexd 6528 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚𝑍) → (𝑥𝐴𝐵) ∈ V)
1613, 12, 15syl2anc 694 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → (𝑥𝐴𝐵) ∈ V)
17 eqid 2651 . . . . . . . . . . . . . . . . . . 19 (𝑚𝑍 ↦ (𝑥𝐴𝐵)) = (𝑚𝑍 ↦ (𝑥𝐴𝐵))
1817fvmpt2 6330 . . . . . . . . . . . . . . . . . 18 ((𝑚𝑍 ∧ (𝑥𝐴𝐵) ∈ V) → ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) = (𝑥𝐴𝐵))
1912, 16, 18syl2anc 694 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) = (𝑥𝐴𝐵))
2019dmeqd 5358 . . . . . . . . . . . . . . . 16 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) = dom (𝑥𝐴𝐵))
21 nfv 1883 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑛𝑍
223, 21nfan 1868 . . . . . . . . . . . . . . . . . . 19 𝑥(𝜑𝑛𝑍)
23 nfv 1883 . . . . . . . . . . . . . . . . . . 19 𝑥 𝑚 ∈ (ℤ𝑛)
2422, 23nfan 1868 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛))
25 simplll 813 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) ∧ 𝑥𝐴) → 𝜑)
2612adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) ∧ 𝑥𝐴) → 𝑚𝑍)
27 simpr 476 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) ∧ 𝑥𝐴) → 𝑥𝐴)
28 smflimmpt.b . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚𝑍𝑥𝐴) → 𝐵𝑊)
2925, 26, 27, 28syl3anc 1366 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) ∧ 𝑥𝐴) → 𝐵𝑊)
30 eqid 2651 . . . . . . . . . . . . . . . . . 18 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
3124, 29, 30fnmptd 39748 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → (𝑥𝐴𝐵) Fn 𝐴)
3231fndmd 39755 . . . . . . . . . . . . . . . 16 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → dom (𝑥𝐴𝐵) = 𝐴)
3320, 32eqtr2d 2686 . . . . . . . . . . . . . . 15 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝐴 = dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
349, 33iineq2d 4573 . . . . . . . . . . . . . 14 ((𝜑𝑛𝑍) → 𝑚 ∈ (ℤ𝑛)𝐴 = 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
356, 34iuneq2df 39526 . . . . . . . . . . . . 13 (𝜑 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 = 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
36 simpr 476 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚𝑍) → 𝑚𝑍)
3736, 15, 18syl2anc 694 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚𝑍) → ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) = (𝑥𝐴𝐵))
3837eqcomd 2657 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚𝑍) → (𝑥𝐴𝐵) = ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
3938dmeqd 5358 . . . . . . . . . . . . . . . 16 ((𝜑𝑚𝑍) → dom (𝑥𝐴𝐵) = dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
4013, 12, 39syl2anc 694 . . . . . . . . . . . . . . 15 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → dom (𝑥𝐴𝐵) = dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
419, 40iineq2d 4573 . . . . . . . . . . . . . 14 ((𝜑𝑛𝑍) → 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) = 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
426, 41iuneq2df 39526 . . . . . . . . . . . . 13 (𝜑 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) = 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
4335, 42eqtr4d 2688 . . . . . . . . . . . 12 (𝜑 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 = 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵))
4443eleq2d 2716 . . . . . . . . . . 11 (𝜑 → (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵)))
4544biimpa 500 . . . . . . . . . 10 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵))
4645adantrr 753 . . . . . . . . 9 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ )) → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵))
47 eliun 4556 . . . . . . . . . . . . 13 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ↔ ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
4847biimpi 206 . . . . . . . . . . . 12 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
4948adantl 481 . . . . . . . . . . 11 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
5049adantrr 753 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ )) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
51 nfv 1883 . . . . . . . . . . . . 13 𝑛(𝑚𝑍𝐵) ∈ dom ⇝
526, 51nfan 1868 . . . . . . . . . . . 12 𝑛(𝜑 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ )
53 nfv 1883 . . . . . . . . . . . 12 𝑛(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝
54 simpllr 815 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ ) ∧ 𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → (𝑚𝑍𝐵) ∈ dom ⇝ )
55 nfcv 2793 . . . . . . . . . . . . . . . . . 18 𝑚𝑥
56 nfii1 4583 . . . . . . . . . . . . . . . . . 18 𝑚 𝑚 ∈ (ℤ𝑛)𝐴
5755, 56nfel 2806 . . . . . . . . . . . . . . . . 17 𝑚 𝑥 𝑚 ∈ (ℤ𝑛)𝐴
589, 57nfan 1868 . . . . . . . . . . . . . . . 16 𝑚((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
5910eluzelz2 39940 . . . . . . . . . . . . . . . . 17 (𝑛𝑍𝑛 ∈ ℤ)
6059ad2antlr 763 . . . . . . . . . . . . . . . 16 (((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑛 ∈ ℤ)
61 eqid 2651 . . . . . . . . . . . . . . . 16 (ℤ𝑛) = (ℤ𝑛)
6210fvexi 6240 . . . . . . . . . . . . . . . . 17 𝑍 ∈ V
6362a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑍 ∈ V)
6410uzssd3 39966 . . . . . . . . . . . . . . . . 17 (𝑛𝑍 → (ℤ𝑛) ⊆ 𝑍)
6564ad2antlr 763 . . . . . . . . . . . . . . . 16 (((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → (ℤ𝑛) ⊆ 𝑍)
66 fvexd 6241 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝑥𝐴𝐵)‘𝑥) ∈ V)
67 eliinid 39608 . . . . . . . . . . . . . . . . . 18 ((𝑥 𝑚 ∈ (ℤ𝑛)𝐴𝑚 ∈ (ℤ𝑛)) → 𝑥𝐴)
6867adantll 750 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑥𝐴)
6913adantlr 751 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝜑)
7012adantlr 751 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
7169, 70, 68, 28syl3anc 1366 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝐵𝑊)
7230fvmpt2 6330 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴𝐵𝑊) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
7368, 71, 72syl2anc 694 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
7458, 60, 61, 63, 63, 65, 65, 66, 73climeldmeqmpt3 40239 . . . . . . . . . . . . . . 15 (((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → ((𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ↔ (𝑚𝑍𝐵) ∈ dom ⇝ ))
7574adantllr 755 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ ) ∧ 𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → ((𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ↔ (𝑚𝑍𝐵) ∈ dom ⇝ ))
7654, 75mpbird 247 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ ) ∧ 𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )
7776exp31 629 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ ) → (𝑛𝑍 → (𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )))
7852, 53, 77rexlimd 3055 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ ) → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ))
7978adantrl 752 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ )) → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ))
8050, 79mpd 15 . . . . . . . . 9 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ )) → (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )
8146, 80jca 553 . . . . . . . 8 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ )) → (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ))
8281ex 449 . . . . . . 7 (𝜑 → ((𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ ) → (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )))
8344biimpar 501 . . . . . . . . . 10 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵)) → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴)
8483adantrr 753 . . . . . . . . 9 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )) → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴)
8584, 48syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
866, 53nfan 1868 . . . . . . . . . . . 12 𝑛(𝜑 ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )
87 simpllr 815 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )
8874adantllr 755 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → ((𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ↔ (𝑚𝑍𝐵) ∈ dom ⇝ ))
8987, 88mpbid 222 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → (𝑚𝑍𝐵) ∈ dom ⇝ )
9089exp31 629 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ) → (𝑛𝑍 → (𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → (𝑚𝑍𝐵) ∈ dom ⇝ )))
9186, 51, 90rexlimd 3055 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ) → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → (𝑚𝑍𝐵) ∈ dom ⇝ ))
9291adantrl 752 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )) → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → (𝑚𝑍𝐵) ∈ dom ⇝ ))
9385, 92mpd 15 . . . . . . . . 9 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )) → (𝑚𝑍𝐵) ∈ dom ⇝ )
9484, 93jca 553 . . . . . . . 8 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )) → (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ ))
9594ex 449 . . . . . . 7 (𝜑 → ((𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ) → (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ )))
9682, 95impbid 202 . . . . . 6 (𝜑 → ((𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ ) ↔ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )))
973, 96rabbida3 39634 . . . . 5 (𝜑 → {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (𝑚𝑍𝐵) ∈ dom ⇝ } = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∣ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ })
985, 97eqtrd 2685 . . . 4 (𝜑𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∣ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ })
994eleq2i 2722 . . . . . . . . 9 (𝑥𝐷𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (𝑚𝑍𝐵) ∈ dom ⇝ })
10099biimpi 206 . . . . . . . 8 (𝑥𝐷𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (𝑚𝑍𝐵) ∈ dom ⇝ })
101 rabidim1 3147 . . . . . . . 8 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (𝑚𝑍𝐵) ∈ dom ⇝ } → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴)
102100, 101, 483syl 18 . . . . . . 7 (𝑥𝐷 → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
103102adantl 481 . . . . . 6 ((𝜑𝑥𝐷) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
104 nfcv 2793 . . . . . . . . 9 𝑛𝑥
105 nfiu1 4582 . . . . . . . . . . 11 𝑛 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴
10651, 105nfrab 3153 . . . . . . . . . 10 𝑛{𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (𝑚𝑍𝐵) ∈ dom ⇝ }
1074, 106nfcxfr 2791 . . . . . . . . 9 𝑛𝐷
108104, 107nfel 2806 . . . . . . . 8 𝑛 𝑥𝐷
1096, 108nfan 1868 . . . . . . 7 𝑛(𝜑𝑥𝐷)
110 nfv 1883 . . . . . . 7 𝑛( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥))) = ( ⇝ ‘(𝑚𝑍𝐵))
1117, 8, 57nf3an 1871 . . . . . . . . . 10 𝑚(𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
112 simp2 1082 . . . . . . . . . . 11 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑛𝑍)
113112, 59syl 17 . . . . . . . . . 10 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑛 ∈ ℤ)
11462a1i 11 . . . . . . . . . 10 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑍 ∈ V)
11510, 112uzssd2 39957 . . . . . . . . . 10 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → (ℤ𝑛) ⊆ 𝑍)
116 fvexd 6241 . . . . . . . . . 10 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝑥𝐴𝐵)‘𝑥) ∈ V)
117673ad2antl3 1245 . . . . . . . . . . 11 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑥𝐴)
118 simpl1 1084 . . . . . . . . . . . 12 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝜑)
119112, 11sylan 487 . . . . . . . . . . . 12 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
120118, 119, 117, 28syl3anc 1366 . . . . . . . . . . 11 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝐵𝑊)
121117, 120, 72syl2anc 694 . . . . . . . . . 10 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
122111, 113, 61, 114, 114, 115, 115, 116, 121climfveqmpt3 40232 . . . . . . . . 9 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥))) = ( ⇝ ‘(𝑚𝑍𝐵)))
1231223exp 1283 . . . . . . . 8 (𝜑 → (𝑛𝑍 → (𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥))) = ( ⇝ ‘(𝑚𝑍𝐵)))))
124123adantr 480 . . . . . . 7 ((𝜑𝑥𝐷) → (𝑛𝑍 → (𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥))) = ( ⇝ ‘(𝑚𝑍𝐵)))))
125109, 110, 124rexlimd 3055 . . . . . 6 ((𝜑𝑥𝐷) → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥))) = ( ⇝ ‘(𝑚𝑍𝐵))))
126103, 125mpd 15 . . . . 5 ((𝜑𝑥𝐷) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥))) = ( ⇝ ‘(𝑚𝑍𝐵)))
127126eqcomd 2657 . . . 4 ((𝜑𝑥𝐷) → ( ⇝ ‘(𝑚𝑍𝐵)) = ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥))))
1283, 98, 127mpteq12da 39766 . . 3 (𝜑 → (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍𝐵))) = (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∣ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)))))
12938eqcomd 2657 . . . . . . . . 9 ((𝜑𝑚𝑍) → ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) = (𝑥𝐴𝐵))
130129fveq1d 6231 . . . . . . . 8 ((𝜑𝑚𝑍) → (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥) = ((𝑥𝐴𝐵)‘𝑥))
1317, 130mpteq2da 4776 . . . . . . 7 (𝜑 → (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) = (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)))
132131eqcomd 2657 . . . . . 6 (𝜑 → (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) = (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)))
133132eleq1d 2715 . . . . 5 (𝜑 → ((𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ↔ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ ))
1343, 42, 133rabbida2 39631 . . . 4 (𝜑 → {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∣ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ } = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ })
135130eqcomd 2657 . . . . . 6 ((𝜑𝑚𝑍) → ((𝑥𝐴𝐵)‘𝑥) = (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))
1367, 135mpteq2da 4776 . . . . 5 (𝜑 → (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) = (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)))
137136fveq2d 6233 . . . 4 (𝜑 → ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥))) = ( ⇝ ‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))))
1383, 134, 137mpteq12d 4767 . . 3 (𝜑 → (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∣ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)))) = (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)))))
1392, 128, 1383eqtrd 2689 . 2 (𝜑𝐺 = (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)))))
140 nfmpt1 4780 . . 3 𝑚(𝑚𝑍 ↦ (𝑥𝐴𝐵))
141 nfcv 2793 . . . 4 𝑥𝑍
142 nfmpt1 4780 . . . 4 𝑥(𝑥𝐴𝐵)
143141, 142nfmpt 4779 . . 3 𝑥(𝑚𝑍 ↦ (𝑥𝐴𝐵))
144 smflimmpt.m . . 3 (𝜑𝑀 ∈ ℤ)
145 smflimmpt.s . . 3 (𝜑𝑆 ∈ SAlg)
146 smflimmpt.l . . . 4 ((𝜑𝑚𝑍) → (𝑥𝐴𝐵) ∈ (SMblFn‘𝑆))
1477, 146, 17fmptdf 6427 . . 3 (𝜑 → (𝑚𝑍 ↦ (𝑥𝐴𝐵)):𝑍⟶(SMblFn‘𝑆))
148 eqid 2651 . . 3 {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ }
149 eqid 2651 . . 3 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)))) = (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))))
150140, 143, 144, 10, 145, 147, 148, 149smflim2 41333 . 2 (𝜑 → (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)))) ∈ (SMblFn‘𝑆))
151139, 150eqeltrd 2730 1 (𝜑𝐺 ∈ (SMblFn‘𝑆))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523  Ⅎwnf 1748   ∈ wcel 2030  ∃wrex 2942  {crab 2945  Vcvv 3231   ⊆ wss 3607  ∪ ciun 4552  ∩ ciin 4553   ↦ cmpt 4762  dom cdm 5143  ‘cfv 5926  ℤcz 11415  ℤ≥cuz 11725   ⇝ cli 14259  SAlgcsalg 40846  SMblFncsmblfn 41230 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cc 9295  ax-ac2 9323  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-omul 7610  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-acn 8806  df-ac 8977  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-ioo 12217  df-ico 12219  df-fl 12633  df-seq 12842  df-exp 12901  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-rlim 14264  df-rest 16130  df-salg 40847  df-smblfn 41231 This theorem is referenced by:  smflimsuplem3  41349
 Copyright terms: Public domain W3C validator