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

Theorem fnlimfvre 40391
Description: The limit function of real functions, applied to elements in its domain, evaluates to Real values. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypotheses
Ref Expression
fnlimfvre.p 𝑚𝜑
fnlimfvre.m 𝑚𝐹
fnlimfvre.n 𝑥𝐹
fnlimfvre.z 𝑍 = (ℤ𝑀)
fnlimfvre.f ((𝜑𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
fnlimfvre.d 𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
fnlimfvre.x (𝜑𝑋𝐷)
Assertion
Ref Expression
fnlimfvre (𝜑 → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))) ∈ ℝ)
Distinct variable groups:   𝑛,𝐹   𝑚,𝑋,𝑛,𝑥   𝑚,𝑍,𝑛,𝑥   𝜑,𝑛
Allowed substitution hints:   𝜑(𝑥,𝑚)   𝐷(𝑥,𝑚,𝑛)   𝐹(𝑥,𝑚)   𝑀(𝑥,𝑚,𝑛)

Proof of Theorem fnlimfvre
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 fnlimfvre.x . . 3 (𝜑𝑋𝐷)
2 fnlimfvre.d . . . . . 6 𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
3 nfcv 2959 . . . . . . . 8 𝑥𝑍
4 nfcv 2959 . . . . . . . . 9 𝑥(ℤ𝑛)
5 fnlimfvre.n . . . . . . . . . . 11 𝑥𝐹
6 nfcv 2959 . . . . . . . . . . 11 𝑥𝑚
75, 6nffv 6425 . . . . . . . . . 10 𝑥(𝐹𝑚)
87nfdm 5579 . . . . . . . . 9 𝑥dom (𝐹𝑚)
94, 8nfiin 4752 . . . . . . . 8 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
103, 9nfiun 4751 . . . . . . 7 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
1110ssrab2f 39797 . . . . . 6 {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } ⊆ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
122, 11eqsstri 3843 . . . . 5 𝐷 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
1312sseli 3805 . . . 4 (𝑋𝐷𝑋 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
14 eliun 4727 . . . 4 (𝑋 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ↔ ∃𝑛𝑍 𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
1513, 14sylib 209 . . 3 (𝑋𝐷 → ∃𝑛𝑍 𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
161, 15syl 17 . 2 (𝜑 → ∃𝑛𝑍 𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
17 nfv 2005 . . 3 𝑛𝜑
18 nfv 2005 . . 3 𝑛( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))) ∈ ℝ
19 fnlimfvre.p . . . . . . 7 𝑚𝜑
20 nfv 2005 . . . . . . 7 𝑚 𝑛𝑍
21 nfcv 2959 . . . . . . . 8 𝑚𝑋
22 nfii1 4754 . . . . . . . 8 𝑚 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
2321, 22nfel 2972 . . . . . . 7 𝑚 𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
2419, 20, 23nf3an 1993 . . . . . 6 𝑚(𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
25 uzssz 11931 . . . . . . . 8 (ℤ𝑀) ⊆ ℤ
26 fnlimfvre.z . . . . . . . . . 10 𝑍 = (ℤ𝑀)
2726eleq2i 2888 . . . . . . . . 9 (𝑛𝑍𝑛 ∈ (ℤ𝑀))
2827biimpi 207 . . . . . . . 8 (𝑛𝑍𝑛 ∈ (ℤ𝑀))
2925, 28sseldi 3807 . . . . . . 7 (𝑛𝑍𝑛 ∈ ℤ)
30293ad2ant2 1157 . . . . . 6 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑛 ∈ ℤ)
31 eqid 2817 . . . . . 6 (ℤ𝑛) = (ℤ𝑛)
3226fvexi 6429 . . . . . . 7 𝑍 ∈ V
3332a1i 11 . . . . . 6 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑍 ∈ V)
3426uztrn2 11929 . . . . . . . 8 ((𝑛𝑍𝑗 ∈ (ℤ𝑛)) → 𝑗𝑍)
3534ssd 39750 . . . . . . 7 (𝑛𝑍 → (ℤ𝑛) ⊆ 𝑍)
36353ad2ant2 1157 . . . . . 6 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (ℤ𝑛) ⊆ 𝑍)
37 fvexd 6430 . . . . . 6 (((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑚𝑍) → ((𝐹𝑚)‘𝑋) ∈ V)
38 fvexd 6430 . . . . . 6 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (ℤ𝑛) ∈ V)
39 ssidd 3832 . . . . . 6 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (ℤ𝑛) ⊆ (ℤ𝑛))
40 fvexd 6430 . . . . . 6 (((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝐹𝑚)‘𝑋) ∈ V)
41 eqidd 2818 . . . . . 6 (((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝐹𝑚)‘𝑋) = ((𝐹𝑚)‘𝑋))
4224, 30, 31, 33, 36, 37, 38, 39, 40, 41climfveqmpt 40388 . . . . 5 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))) = ( ⇝ ‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))))
432eleq2i 2888 . . . . . . . . . . . . 13 (𝑋𝐷𝑋 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ })
4443biimpi 207 . . . . . . . . . . . 12 (𝑋𝐷𝑋 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ })
45 nfcv 2959 . . . . . . . . . . . . . . 15 𝑥𝑋
467, 45nffv 6425 . . . . . . . . . . . . . . . . 17 𝑥((𝐹𝑚)‘𝑋)
473, 46nfmpt 4951 . . . . . . . . . . . . . . . 16 𝑥(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))
48 nfcv 2959 . . . . . . . . . . . . . . . 16 𝑥dom ⇝
4947, 48nfel 2972 . . . . . . . . . . . . . . 15 𝑥(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝
50 fveq2 6415 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → ((𝐹𝑚)‘𝑥) = ((𝐹𝑚)‘𝑋))
5150mpteq2dv 4950 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)))
5251eleq1d 2881 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ ))
5345, 10, 49, 52elrabf 3566 . . . . . . . . . . . . . 14 (𝑋 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } ↔ (𝑋 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ ))
5453biimpi 207 . . . . . . . . . . . . 13 (𝑋 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } → (𝑋 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ ))
5554simprd 485 . . . . . . . . . . . 12 (𝑋 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ )
5644, 55syl 17 . . . . . . . . . . 11 (𝑋𝐷 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ )
5756adantr 468 . . . . . . . . . 10 ((𝑋𝐷𝑛𝑍) → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ )
58 nfmpt1 4952 . . . . . . . . . . . . . . . 16 𝑚(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))
59 nfcv 2959 . . . . . . . . . . . . . . . 16 𝑚dom ⇝
6058, 59nfel 2972 . . . . . . . . . . . . . . 15 𝑚(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝
61 nfv 2005 . . . . . . . . . . . . . . . . 17 𝑚 𝑗𝑍
6261nfci 2949 . . . . . . . . . . . . . . . 16 𝑚𝑍
6362, 22nfiun 4751 . . . . . . . . . . . . . . 15 𝑚 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
6460, 63nfrab 3323 . . . . . . . . . . . . . 14 𝑚{𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
652, 64nfcxfr 2957 . . . . . . . . . . . . 13 𝑚𝐷
6621, 65nfel 2972 . . . . . . . . . . . 12 𝑚 𝑋𝐷
6766, 20nfan 1990 . . . . . . . . . . 11 𝑚(𝑋𝐷𝑛𝑍)
6829adantl 469 . . . . . . . . . . 11 ((𝑋𝐷𝑛𝑍) → 𝑛 ∈ ℤ)
6932a1i 11 . . . . . . . . . . 11 ((𝑋𝐷𝑛𝑍) → 𝑍 ∈ V)
7035adantl 469 . . . . . . . . . . 11 ((𝑋𝐷𝑛𝑍) → (ℤ𝑛) ⊆ 𝑍)
71 fvexd 6430 . . . . . . . . . . 11 (((𝑋𝐷𝑛𝑍) ∧ 𝑚𝑍) → ((𝐹𝑚)‘𝑋) ∈ V)
72 fvexd 6430 . . . . . . . . . . 11 ((𝑋𝐷𝑛𝑍) → (ℤ𝑛) ∈ V)
73 ssidd 3832 . . . . . . . . . . 11 ((𝑋𝐷𝑛𝑍) → (ℤ𝑛) ⊆ (ℤ𝑛))
74 fvexd 6430 . . . . . . . . . . 11 (((𝑋𝐷𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝐹𝑚)‘𝑋) ∈ V)
75 eqidd 2818 . . . . . . . . . . 11 (((𝑋𝐷𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝐹𝑚)‘𝑋) = ((𝐹𝑚)‘𝑋))
7667, 68, 31, 69, 70, 71, 72, 73, 74, 75climeldmeqmpt 40385 . . . . . . . . . 10 ((𝑋𝐷𝑛𝑍) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ ↔ (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ ))
7757, 76mpbid 223 . . . . . . . . 9 ((𝑋𝐷𝑛𝑍) → (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ )
78 climdm 14515 . . . . . . . . 9 ((𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ ↔ (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) ⇝ ( ⇝ ‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))))
7977, 78sylib 209 . . . . . . . 8 ((𝑋𝐷𝑛𝑍) → (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) ⇝ ( ⇝ ‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))))
801, 79sylan 571 . . . . . . 7 ((𝜑𝑛𝑍) → (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) ⇝ ( ⇝ ‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))))
81803adant3 1155 . . . . . 6 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) ⇝ ( ⇝ ‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))))
82 simpl1 1235 . . . . . . 7 (((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝜑)
83 simpl2 1237 . . . . . . 7 (((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑛𝑍)
84 nfcv 2959 . . . . . . . . . . . . 13 𝑗dom (𝐹𝑚)
85 fnlimfvre.m . . . . . . . . . . . . . . 15 𝑚𝐹
86 nfcv 2959 . . . . . . . . . . . . . . 15 𝑚𝑗
8785, 86nffv 6425 . . . . . . . . . . . . . 14 𝑚(𝐹𝑗)
8887nfdm 5579 . . . . . . . . . . . . 13 𝑚dom (𝐹𝑗)
89 fveq2 6415 . . . . . . . . . . . . . 14 (𝑚 = 𝑗 → (𝐹𝑚) = (𝐹𝑗))
9089dmeqd 5538 . . . . . . . . . . . . 13 (𝑚 = 𝑗 → dom (𝐹𝑚) = dom (𝐹𝑗))
9184, 88, 90cbviin 4761 . . . . . . . . . . . 12 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑗 ∈ (ℤ𝑛)dom (𝐹𝑗)
9291eleq2i 2888 . . . . . . . . . . 11 (𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ↔ 𝑋 𝑗 ∈ (ℤ𝑛)dom (𝐹𝑗))
9392biimpi 207 . . . . . . . . . 10 (𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → 𝑋 𝑗 ∈ (ℤ𝑛)dom (𝐹𝑗))
9493adantr 468 . . . . . . . . 9 ((𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑋 𝑗 ∈ (ℤ𝑛)dom (𝐹𝑗))
95 simpr 473 . . . . . . . . 9 ((𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑗 ∈ (ℤ𝑛))
96 eliinid 39791 . . . . . . . . 9 ((𝑋 𝑗 ∈ (ℤ𝑛)dom (𝐹𝑗) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑋 ∈ dom (𝐹𝑗))
9794, 95, 96syl2anc 575 . . . . . . . 8 ((𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑋 ∈ dom (𝐹𝑗))
98973ad2antl3 1231 . . . . . . 7 (((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑋 ∈ dom (𝐹𝑗))
99 simpr 473 . . . . . . 7 (((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑗 ∈ (ℤ𝑛))
100 id 22 . . . . . . . . . 10 (𝑗 ∈ (ℤ𝑛) → 𝑗 ∈ (ℤ𝑛))
101 fvexd 6430 . . . . . . . . . 10 (𝑗 ∈ (ℤ𝑛) → ((𝐹𝑗)‘𝑋) ∈ V)
10287, 21nffv 6425 . . . . . . . . . . 11 𝑚((𝐹𝑗)‘𝑋)
10389fveq1d 6417 . . . . . . . . . . 11 (𝑚 = 𝑗 → ((𝐹𝑚)‘𝑋) = ((𝐹𝑗)‘𝑋))
104 eqid 2817 . . . . . . . . . . 11 (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) = (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))
10586, 102, 103, 104fvmptf 6529 . . . . . . . . . 10 ((𝑗 ∈ (ℤ𝑛) ∧ ((𝐹𝑗)‘𝑋) ∈ V) → ((𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))‘𝑗) = ((𝐹𝑗)‘𝑋))
106100, 101, 105syl2anc 575 . . . . . . . . 9 (𝑗 ∈ (ℤ𝑛) → ((𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))‘𝑗) = ((𝐹𝑗)‘𝑋))
107106adantl 469 . . . . . . . 8 (((𝜑𝑛𝑍𝑋 ∈ dom (𝐹𝑗)) ∧ 𝑗 ∈ (ℤ𝑛)) → ((𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))‘𝑗) = ((𝐹𝑗)‘𝑋))
108 simpll 774 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝜑)
10934adantll 696 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑗𝑍)
11019, 61nfan 1990 . . . . . . . . . . . . 13 𝑚(𝜑𝑗𝑍)
111 nfcv 2959 . . . . . . . . . . . . . 14 𝑚
11287, 88, 111nff 6259 . . . . . . . . . . . . 13 𝑚(𝐹𝑗):dom (𝐹𝑗)⟶ℝ
113110, 112nfim 1987 . . . . . . . . . . . 12 𝑚((𝜑𝑗𝑍) → (𝐹𝑗):dom (𝐹𝑗)⟶ℝ)
114 eleq1w 2879 . . . . . . . . . . . . . 14 (𝑚 = 𝑗 → (𝑚𝑍𝑗𝑍))
115114anbi2d 616 . . . . . . . . . . . . 13 (𝑚 = 𝑗 → ((𝜑𝑚𝑍) ↔ (𝜑𝑗𝑍)))
11689, 90feq12d 6251 . . . . . . . . . . . . 13 (𝑚 = 𝑗 → ((𝐹𝑚):dom (𝐹𝑚)⟶ℝ ↔ (𝐹𝑗):dom (𝐹𝑗)⟶ℝ))
117115, 116imbi12d 335 . . . . . . . . . . . 12 (𝑚 = 𝑗 → (((𝜑𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ) ↔ ((𝜑𝑗𝑍) → (𝐹𝑗):dom (𝐹𝑗)⟶ℝ)))
118 fnlimfvre.f . . . . . . . . . . . 12 ((𝜑𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
119113, 117, 118chvar 2438 . . . . . . . . . . 11 ((𝜑𝑗𝑍) → (𝐹𝑗):dom (𝐹𝑗)⟶ℝ)
120108, 109, 119syl2anc 575 . . . . . . . . . 10 (((𝜑𝑛𝑍) ∧ 𝑗 ∈ (ℤ𝑛)) → (𝐹𝑗):dom (𝐹𝑗)⟶ℝ)
1211203adantl3 1202 . . . . . . . . 9 (((𝜑𝑛𝑍𝑋 ∈ dom (𝐹𝑗)) ∧ 𝑗 ∈ (ℤ𝑛)) → (𝐹𝑗):dom (𝐹𝑗)⟶ℝ)
122 simpl3 1239 . . . . . . . . 9 (((𝜑𝑛𝑍𝑋 ∈ dom (𝐹𝑗)) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑋 ∈ dom (𝐹𝑗))
123121, 122ffvelrnd 6589 . . . . . . . 8 (((𝜑𝑛𝑍𝑋 ∈ dom (𝐹𝑗)) ∧ 𝑗 ∈ (ℤ𝑛)) → ((𝐹𝑗)‘𝑋) ∈ ℝ)
124107, 123eqeltrd 2896 . . . . . . 7 (((𝜑𝑛𝑍𝑋 ∈ dom (𝐹𝑗)) ∧ 𝑗 ∈ (ℤ𝑛)) → ((𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))‘𝑗) ∈ ℝ)
12582, 83, 98, 99, 124syl31anc 1485 . . . . . 6 (((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑗 ∈ (ℤ𝑛)) → ((𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))‘𝑗) ∈ ℝ)
12631, 30, 81, 125climrecl 14544 . . . . 5 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → ( ⇝ ‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))) ∈ ℝ)
12742, 126eqeltrd 2896 . . . 4 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))) ∈ ℝ)
1281273exp 1141 . . 3 (𝜑 → (𝑛𝑍 → (𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))) ∈ ℝ)))
12917, 18, 128rexlimd 3225 . 2 (𝜑 → (∃𝑛𝑍 𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))) ∈ ℝ))
13016, 129mpd 15 1 (𝜑 → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100   = wceq 1637  wnf 1863  wcel 2157  wnfc 2946  wrex 3108  {crab 3111  Vcvv 3402  wss 3780   ciun 4723   ciin 4724   class class class wbr 4855  cmpt 4934  dom cdm 5322  wf 6104  cfv 6108  cr 10227  cz 11650  cuz 11911  cli 14445
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4975  ax-sep 4986  ax-nul 4994  ax-pow 5046  ax-pr 5107  ax-un 7186  ax-cnex 10284  ax-resscn 10285  ax-1cn 10286  ax-icn 10287  ax-addcl 10288  ax-addrcl 10289  ax-mulcl 10290  ax-mulrcl 10291  ax-mulcom 10292  ax-addass 10293  ax-mulass 10294  ax-distr 10295  ax-i2m1 10296  ax-1ne0 10297  ax-1rid 10298  ax-rnegex 10299  ax-rrecex 10300  ax-cnre 10301  ax-pre-lttri 10302  ax-pre-lttrn 10303  ax-pre-ltadd 10304  ax-pre-mulgt0 10305  ax-pre-sup 10306
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-iun 4725  df-iin 4726  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5230  df-eprel 5235  df-po 5243  df-so 5244  df-fr 5281  df-we 5283  df-xp 5328  df-rel 5329  df-cnv 5330  df-co 5331  df-dm 5332  df-rn 5333  df-res 5334  df-ima 5335  df-pred 5904  df-ord 5950  df-on 5951  df-lim 5952  df-suc 5953  df-iota 6071  df-fun 6110  df-fn 6111  df-f 6112  df-f1 6113  df-fo 6114  df-f1o 6115  df-fv 6116  df-riota 6842  df-ov 6884  df-oprab 6885  df-mpt2 6886  df-om 7303  df-2nd 7406  df-wrecs 7649  df-recs 7711  df-rdg 7749  df-er 7986  df-pm 8102  df-en 8200  df-dom 8201  df-sdom 8202  df-sup 8594  df-inf 8595  df-pnf 10368  df-mnf 10369  df-xr 10370  df-ltxr 10371  df-le 10372  df-sub 10560  df-neg 10561  df-div 10977  df-nn 11313  df-2 11371  df-3 11372  df-n0 11567  df-z 11651  df-uz 11912  df-rp 12054  df-fl 12824  df-seq 13032  df-exp 13091  df-cj 14069  df-re 14070  df-im 14071  df-sqrt 14205  df-abs 14206  df-clim 14449  df-rlim 14450
This theorem is referenced by:  fnlimfvre2  40394  fnlimf  40395  smflimlem4  41469  smflim  41472
  Copyright terms: Public domain W3C validator