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

Theorem smflimmpt 41588
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 indices 𝐵(𝑚, 𝑥). (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 2009 . . . . . . . . . . . . . . . 16 𝑚 𝑛𝑍
97, 8nfan 1998 . . . . . . . . . . . . . . 15 𝑚(𝜑𝑛𝑍)
10 smflimmpt.z . . . . . . . . . . . . . . . . . . . 20 𝑍 = (ℤ𝑀)
1110uztrn2 11903 . . . . . . . . . . . . . . . . . . 19 ((𝑛𝑍𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
1211adantll 705 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
13 simpll 783 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝜑)
14 smflimmpt.a . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚𝑍) → 𝐴𝑉)
1514mptexd 6679 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚𝑍) → (𝑥𝐴𝐵) ∈ V)
1613, 12, 15syl2anc 579 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → (𝑥𝐴𝐵) ∈ V)
17 eqid 2764 . . . . . . . . . . . . . . . . . . 19 (𝑚𝑍 ↦ (𝑥𝐴𝐵)) = (𝑚𝑍 ↦ (𝑥𝐴𝐵))
1817fvmpt2 6479 . . . . . . . . . . . . . . . . . 18 ((𝑚𝑍 ∧ (𝑥𝐴𝐵) ∈ V) → ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) = (𝑥𝐴𝐵))
1912, 16, 18syl2anc 579 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) = (𝑥𝐴𝐵))
2019dmeqd 5493 . . . . . . . . . . . . . . . 16 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) = dom (𝑥𝐴𝐵))
21 nfv 2009 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑛𝑍
223, 21nfan 1998 . . . . . . . . . . . . . . . . . . 19 𝑥(𝜑𝑛𝑍)
23 nfv 2009 . . . . . . . . . . . . . . . . . . 19 𝑥 𝑚 ∈ (ℤ𝑛)
2422, 23nfan 1998 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛))
25 simplll 791 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) ∧ 𝑥𝐴) → 𝜑)
2612adantr 472 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) ∧ 𝑥𝐴) → 𝑚𝑍)
27 simpr 477 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) ∧ 𝑥𝐴) → 𝑥𝐴)
28 smflimmpt.b . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚𝑍𝑥𝐴) → 𝐵𝑊)
2925, 26, 27, 28syl3anc 1490 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) ∧ 𝑥𝐴) → 𝐵𝑊)
30 eqid 2764 . . . . . . . . . . . . . . . . . 18 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
3124, 29, 30fnmptd 40008 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → (𝑥𝐴𝐵) Fn 𝐴)
3231fndmd 40015 . . . . . . . . . . . . . . . 16 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → dom (𝑥𝐴𝐵) = 𝐴)
3320, 32eqtr2d 2799 . . . . . . . . . . . . . . 15 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝐴 = dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
349, 33iineq2d 4696 . . . . . . . . . . . . . 14 ((𝜑𝑛𝑍) → 𝑚 ∈ (ℤ𝑛)𝐴 = 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
356, 34iuneq2df 39795 . . . . . . . . . . . . 13 (𝜑 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 = 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
36 simpr 477 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚𝑍) → 𝑚𝑍)
3736, 15, 18syl2anc 579 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚𝑍) → ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) = (𝑥𝐴𝐵))
3837eqcomd 2770 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚𝑍) → (𝑥𝐴𝐵) = ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
3938dmeqd 5493 . . . . . . . . . . . . . . . 16 ((𝜑𝑚𝑍) → dom (𝑥𝐴𝐵) = dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
4013, 12, 39syl2anc 579 . . . . . . . . . . . . . . 15 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → dom (𝑥𝐴𝐵) = dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
419, 40iineq2d 4696 . . . . . . . . . . . . . 14 ((𝜑𝑛𝑍) → 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) = 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
426, 41iuneq2df 39795 . . . . . . . . . . . . 13 (𝜑 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) = 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
4335, 42eqtr4d 2801 . . . . . . . . . . . 12 (𝜑 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 = 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵))
4443eleq2d 2829 . . . . . . . . . . 11 (𝜑 → (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵)))
4544biimpa 468 . . . . . . . . . 10 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵))
4645adantrr 708 . . . . . . . . 9 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ )) → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵))
47 eliun 4679 . . . . . . . . . . . . 13 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ↔ ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
4847biimpi 207 . . . . . . . . . . . 12 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
4948adantl 473 . . . . . . . . . . 11 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
5049adantrr 708 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ )) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
51 nfv 2009 . . . . . . . . . . . . 13 𝑛(𝑚𝑍𝐵) ∈ dom ⇝
526, 51nfan 1998 . . . . . . . . . . . 12 𝑛(𝜑 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ )
53 nfv 2009 . . . . . . . . . . . 12 𝑛(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝
54 simpllr 793 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ ) ∧ 𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → (𝑚𝑍𝐵) ∈ dom ⇝ )
55 nfcv 2906 . . . . . . . . . . . . . . . . . 18 𝑚𝑥
56 nfii1 4706 . . . . . . . . . . . . . . . . . 18 𝑚 𝑚 ∈ (ℤ𝑛)𝐴
5755, 56nfel 2919 . . . . . . . . . . . . . . . . 17 𝑚 𝑥 𝑚 ∈ (ℤ𝑛)𝐴
589, 57nfan 1998 . . . . . . . . . . . . . . . 16 𝑚((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
5910eluzelz2 40196 . . . . . . . . . . . . . . . . 17 (𝑛𝑍𝑛 ∈ ℤ)
6059ad2antlr 718 . . . . . . . . . . . . . . . 16 (((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑛 ∈ ℤ)
61 eqid 2764 . . . . . . . . . . . . . . . 16 (ℤ𝑛) = (ℤ𝑛)
6210fvexi 6388 . . . . . . . . . . . . . . . . 17 𝑍 ∈ V
6362a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑍 ∈ V)
6410uzssd3 40222 . . . . . . . . . . . . . . . . 17 (𝑛𝑍 → (ℤ𝑛) ⊆ 𝑍)
6564ad2antlr 718 . . . . . . . . . . . . . . . 16 (((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → (ℤ𝑛) ⊆ 𝑍)
66 fvexd 6389 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝑥𝐴𝐵)‘𝑥) ∈ V)
67 eliinid 39876 . . . . . . . . . . . . . . . . . 18 ((𝑥 𝑚 ∈ (ℤ𝑛)𝐴𝑚 ∈ (ℤ𝑛)) → 𝑥𝐴)
6867adantll 705 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑥𝐴)
6913adantlr 706 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝜑)
7012adantlr 706 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
7169, 70, 68, 28syl3anc 1490 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝐵𝑊)
7230fvmpt2 6479 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴𝐵𝑊) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
7368, 71, 72syl2anc 579 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
7458, 60, 61, 63, 63, 65, 65, 66, 73climeldmeqmpt3 40491 . . . . . . . . . . . . . . 15 (((𝜑𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → ((𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ↔ (𝑚𝑍𝐵) ∈ dom ⇝ ))
7574adantllr 710 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ ) ∧ 𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → ((𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ↔ (𝑚𝑍𝐵) ∈ dom ⇝ ))
7654, 75mpbird 248 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ ) ∧ 𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )
7776exp31 410 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ ) → (𝑛𝑍 → (𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )))
7852, 53, 77rexlimd 3172 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ ) → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ))
7978adantrl 707 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ )) → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ))
8050, 79mpd 15 . . . . . . . . 9 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ )) → (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )
8146, 80jca 507 . . . . . . . 8 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ )) → (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ))
8281ex 401 . . . . . . 7 (𝜑 → ((𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ ) → (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )))
8344biimpar 469 . . . . . . . . . 10 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵)) → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴)
8483adantrr 708 . . . . . . . . 9 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )) → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴)
8584, 48syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
866, 53nfan 1998 . . . . . . . . . . . 12 𝑛(𝜑 ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )
87 simpllr 793 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )
8874adantllr 710 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → ((𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ↔ (𝑚𝑍𝐵) ∈ dom ⇝ ))
8987, 88mpbid 223 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → (𝑚𝑍𝐵) ∈ dom ⇝ )
9089exp31 410 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ) → (𝑛𝑍 → (𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → (𝑚𝑍𝐵) ∈ dom ⇝ )))
9186, 51, 90rexlimd 3172 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ) → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → (𝑚𝑍𝐵) ∈ dom ⇝ ))
9291adantrl 707 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )) → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → (𝑚𝑍𝐵) ∈ dom ⇝ ))
9385, 92mpd 15 . . . . . . . . 9 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )) → (𝑚𝑍𝐵) ∈ dom ⇝ )
9484, 93jca 507 . . . . . . . 8 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )) → (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ ))
9594ex 401 . . . . . . 7 (𝜑 → ((𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ) → (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ )))
9682, 95impbid 203 . . . . . 6 (𝜑 → ((𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (𝑚𝑍𝐵) ∈ dom ⇝ ) ↔ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∧ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ )))
973, 96rabbida3 39901 . . . . 5 (𝜑 → {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (𝑚𝑍𝐵) ∈ dom ⇝ } = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∣ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ })
985, 97eqtrd 2798 . . . 4 (𝜑𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∣ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ })
994eleq2i 2835 . . . . . . . . 9 (𝑥𝐷𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (𝑚𝑍𝐵) ∈ dom ⇝ })
10099biimpi 207 . . . . . . . 8 (𝑥𝐷𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (𝑚𝑍𝐵) ∈ dom ⇝ })
101 rabidim1 3264 . . . . . . . 8 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (𝑚𝑍𝐵) ∈ dom ⇝ } → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴)
102100, 101, 483syl 18 . . . . . . 7 (𝑥𝐷 → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
103102adantl 473 . . . . . 6 ((𝜑𝑥𝐷) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
104 nfcv 2906 . . . . . . . . 9 𝑛𝑥
105 nfiu1 4705 . . . . . . . . . . 11 𝑛 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴
10651, 105nfrab 3270 . . . . . . . . . 10 𝑛{𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (𝑚𝑍𝐵) ∈ dom ⇝ }
1074, 106nfcxfr 2904 . . . . . . . . 9 𝑛𝐷
108104, 107nfel 2919 . . . . . . . 8 𝑛 𝑥𝐷
1096, 108nfan 1998 . . . . . . 7 𝑛(𝜑𝑥𝐷)
110 nfv 2009 . . . . . . 7 𝑛( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥))) = ( ⇝ ‘(𝑚𝑍𝐵))
1117, 8, 57nf3an 2000 . . . . . . . . . 10 𝑚(𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
112 simp2 1167 . . . . . . . . . . 11 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑛𝑍)
113112, 59syl 17 . . . . . . . . . 10 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑛 ∈ ℤ)
11462a1i 11 . . . . . . . . . 10 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑍 ∈ V)
11510, 112uzssd2 40213 . . . . . . . . . 10 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → (ℤ𝑛) ⊆ 𝑍)
116 fvexd 6389 . . . . . . . . . 10 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝑥𝐴𝐵)‘𝑥) ∈ V)
117673ad2antl3 1238 . . . . . . . . . . 11 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑥𝐴)
118 simpl1 1242 . . . . . . . . . . . 12 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝜑)
119112, 11sylan 575 . . . . . . . . . . . 12 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
120118, 119, 117, 28syl3anc 1490 . . . . . . . . . . 11 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝐵𝑊)
121117, 120, 72syl2anc 579 . . . . . . . . . 10 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
122111, 113, 61, 114, 114, 115, 115, 116, 121climfveqmpt3 40484 . . . . . . . . 9 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥))) = ( ⇝ ‘(𝑚𝑍𝐵)))
1231223exp 1148 . . . . . . . 8 (𝜑 → (𝑛𝑍 → (𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥))) = ( ⇝ ‘(𝑚𝑍𝐵)))))
124123adantr 472 . . . . . . 7 ((𝜑𝑥𝐷) → (𝑛𝑍 → (𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥))) = ( ⇝ ‘(𝑚𝑍𝐵)))))
125109, 110, 124rexlimd 3172 . . . . . 6 ((𝜑𝑥𝐷) → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥))) = ( ⇝ ‘(𝑚𝑍𝐵))))
126103, 125mpd 15 . . . . 5 ((𝜑𝑥𝐷) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥))) = ( ⇝ ‘(𝑚𝑍𝐵)))
127126eqcomd 2770 . . . 4 ((𝜑𝑥𝐷) → ( ⇝ ‘(𝑚𝑍𝐵)) = ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥))))
1283, 98, 127mpteq12da 40026 . . 3 (𝜑 → (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍𝐵))) = (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∣ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)))))
12938eqcomd 2770 . . . . . . . . 9 ((𝜑𝑚𝑍) → ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) = (𝑥𝐴𝐵))
130129fveq1d 6376 . . . . . . . 8 ((𝜑𝑚𝑍) → (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥) = ((𝑥𝐴𝐵)‘𝑥))
1317, 130mpteq2da 4901 . . . . . . 7 (𝜑 → (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) = (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)))
132131eqcomd 2770 . . . . . 6 (𝜑 → (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) = (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)))
133132eleq1d 2828 . . . . 5 (𝜑 → ((𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ ↔ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ ))
1343, 42, 133rabbida2 39898 . . . 4 (𝜑 → {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∣ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ } = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ })
135130eqcomd 2770 . . . . . 6 ((𝜑𝑚𝑍) → ((𝑥𝐴𝐵)‘𝑥) = (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))
1367, 135mpteq2da 4901 . . . . 5 (𝜑 → (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) = (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)))
137136fveq2d 6378 . . . 4 (𝜑 → ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥))) = ( ⇝ ‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))))
1383, 134, 137mpteq12d 4892 . . 3 (𝜑 → (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝑥𝐴𝐵) ∣ (𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝑥𝐴𝐵)‘𝑥)))) = (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)))))
1392, 128, 1383eqtrd 2802 . 2 (𝜑𝐺 = (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)))))
140 nfmpt1 4905 . . 3 𝑚(𝑚𝑍 ↦ (𝑥𝐴𝐵))
141 nfcv 2906 . . . 4 𝑥𝑍
142 nfmpt1 4905 . . . 4 𝑥(𝑥𝐴𝐵)
143141, 142nfmpt 4904 . . 3 𝑥(𝑚𝑍 ↦ (𝑥𝐴𝐵))
144 smflimmpt.m . . 3 (𝜑𝑀 ∈ ℤ)
145 smflimmpt.s . . 3 (𝜑𝑆 ∈ SAlg)
146 smflimmpt.l . . . 4 ((𝜑𝑚𝑍) → (𝑥𝐴𝐵) ∈ (SMblFn‘𝑆))
1477, 146, 17fmptdf 6576 . . 3 (𝜑 → (𝑚𝑍 ↦ (𝑥𝐴𝐵)):𝑍⟶(SMblFn‘𝑆))
148 eqid 2764 . . 3 {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ }
149 eqid 2764 . . 3 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)))) = (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))))
150140, 143, 144, 10, 145, 147, 148, 149smflim2 41584 . 2 (𝜑 → (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)))) ∈ (SMblFn‘𝑆))
151139, 150eqeltrd 2843 1 (𝜑𝐺 ∈ (SMblFn‘𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wnf 1878  wcel 2155  wrex 3055  {crab 3058  Vcvv 3349  wss 3731   ciun 4675   ciin 4676  cmpt 4887  dom cdm 5276  cfv 6067  cz 11623  cuz 11885  cli 14501  SAlgcsalg 41097  SMblFncsmblfn 41481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-inf2 8752  ax-cc 9509  ax-ac2 9537  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265  ax-pre-sup 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-iin 4678  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-se 5236  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-om 7263  df-1st 7365  df-2nd 7366  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-oadd 7767  df-omul 7768  df-er 7946  df-map 8061  df-pm 8062  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-sup 8554  df-inf 8555  df-oi 8621  df-card 9015  df-acn 9018  df-ac 9189  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-div 10938  df-nn 11274  df-2 11334  df-3 11335  df-n0 11538  df-z 11624  df-uz 11886  df-q 11989  df-rp 12028  df-ioo 12380  df-ico 12382  df-fl 12800  df-seq 13008  df-exp 13067  df-cj 14125  df-re 14126  df-im 14127  df-sqrt 14261  df-abs 14262  df-clim 14505  df-rlim 14506  df-rest 16350  df-salg 41098  df-smblfn 41482
This theorem is referenced by:  smflimsuplem3  41600
  Copyright terms: Public domain W3C validator