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 40224
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 2793 . . . . . . . 8 𝑥𝑍
4 nfcv 2793 . . . . . . . . 9 𝑥(ℤ𝑛)
5 fnlimfvre.n . . . . . . . . . . 11 𝑥𝐹
6 nfcv 2793 . . . . . . . . . . 11 𝑥𝑚
75, 6nffv 6236 . . . . . . . . . 10 𝑥(𝐹𝑚)
87nfdm 5399 . . . . . . . . 9 𝑥dom (𝐹𝑚)
94, 8nfiin 4581 . . . . . . . 8 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
103, 9nfiun 4580 . . . . . . 7 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
1110ssrab2f 39614 . . . . . 6 {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } ⊆ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
122, 11eqsstri 3668 . . . . 5 𝐷 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
1312sseli 3632 . . . 4 (𝑋𝐷𝑋 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
14 eliun 4556 . . . 4 (𝑋 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ↔ ∃𝑛𝑍 𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
1513, 14sylib 208 . . 3 (𝑋𝐷 → ∃𝑛𝑍 𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
161, 15syl 17 . 2 (𝜑 → ∃𝑛𝑍 𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
17 nfv 1883 . . 3 𝑛𝜑
18 nfv 1883 . . 3 𝑛( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))) ∈ ℝ
19 fnlimfvre.p . . . . . . 7 𝑚𝜑
20 nfv 1883 . . . . . . 7 𝑚 𝑛𝑍
21 nfcv 2793 . . . . . . . 8 𝑚𝑋
22 nfii1 4583 . . . . . . . 8 𝑚 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
2321, 22nfel 2806 . . . . . . 7 𝑚 𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
2419, 20, 23nf3an 1871 . . . . . 6 𝑚(𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
25 uzssz 11745 . . . . . . . 8 (ℤ𝑀) ⊆ ℤ
26 fnlimfvre.z . . . . . . . . . 10 𝑍 = (ℤ𝑀)
2726eleq2i 2722 . . . . . . . . 9 (𝑛𝑍𝑛 ∈ (ℤ𝑀))
2827biimpi 206 . . . . . . . 8 (𝑛𝑍𝑛 ∈ (ℤ𝑀))
2925, 28sseldi 3634 . . . . . . 7 (𝑛𝑍𝑛 ∈ ℤ)
30293ad2ant2 1103 . . . . . 6 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑛 ∈ ℤ)
31 eqid 2651 . . . . . 6 (ℤ𝑛) = (ℤ𝑛)
32 fvex 6239 . . . . . . . 8 (ℤ𝑀) ∈ V
3326, 32eqeltri 2726 . . . . . . 7 𝑍 ∈ V
3433a1i 11 . . . . . 6 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑍 ∈ V)
3526uztrn2 11743 . . . . . . . 8 ((𝑛𝑍𝑗 ∈ (ℤ𝑛)) → 𝑗𝑍)
3635ssd 39566 . . . . . . 7 (𝑛𝑍 → (ℤ𝑛) ⊆ 𝑍)
37363ad2ant2 1103 . . . . . 6 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (ℤ𝑛) ⊆ 𝑍)
38 fvexd 6241 . . . . . 6 (((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑚𝑍) → ((𝐹𝑚)‘𝑋) ∈ V)
39 fvexd 6241 . . . . . 6 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (ℤ𝑛) ∈ V)
40 simpr 476 . . . . . . 7 (((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑗 ∈ (ℤ𝑛))
4140ssd 39566 . . . . . 6 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (ℤ𝑛) ⊆ (ℤ𝑛))
42 fvexd 6241 . . . . . 6 (((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝐹𝑚)‘𝑋) ∈ V)
43 eqidd 2652 . . . . . 6 (((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝐹𝑚)‘𝑋) = ((𝐹𝑚)‘𝑋))
4424, 30, 31, 34, 37, 38, 39, 41, 42, 43climfveqmpt 40221 . . . . 5 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))) = ( ⇝ ‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))))
452eleq2i 2722 . . . . . . . . . . . . 13 (𝑋𝐷𝑋 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ })
4645biimpi 206 . . . . . . . . . . . 12 (𝑋𝐷𝑋 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ })
47 nfcv 2793 . . . . . . . . . . . . . . 15 𝑥𝑋
487, 47nffv 6236 . . . . . . . . . . . . . . . . 17 𝑥((𝐹𝑚)‘𝑋)
493, 48nfmpt 4779 . . . . . . . . . . . . . . . 16 𝑥(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))
50 nfcv 2793 . . . . . . . . . . . . . . . 16 𝑥dom ⇝
5149, 50nfel 2806 . . . . . . . . . . . . . . 15 𝑥(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝
52 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → ((𝐹𝑚)‘𝑥) = ((𝐹𝑚)‘𝑋))
5352mpteq2dv 4778 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)))
5453eleq1d 2715 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ ))
5547, 10, 51, 54elrabf 3392 . . . . . . . . . . . . . 14 (𝑋 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } ↔ (𝑋 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ ))
5655biimpi 206 . . . . . . . . . . . . 13 (𝑋 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } → (𝑋 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ ))
5756simprd 478 . . . . . . . . . . . 12 (𝑋 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ )
5846, 57syl 17 . . . . . . . . . . 11 (𝑋𝐷 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ )
5958adantr 480 . . . . . . . . . 10 ((𝑋𝐷𝑛𝑍) → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ )
60 nfmpt1 4780 . . . . . . . . . . . . . . . 16 𝑚(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))
61 nfcv 2793 . . . . . . . . . . . . . . . 16 𝑚dom ⇝
6260, 61nfel 2806 . . . . . . . . . . . . . . 15 𝑚(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝
63 nfv 1883 . . . . . . . . . . . . . . . . 17 𝑚 𝑗𝑍
6463nfci 2783 . . . . . . . . . . . . . . . 16 𝑚𝑍
6564, 22nfiun 4580 . . . . . . . . . . . . . . 15 𝑚 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
6662, 65nfrab 3153 . . . . . . . . . . . . . 14 𝑚{𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
672, 66nfcxfr 2791 . . . . . . . . . . . . 13 𝑚𝐷
6821, 67nfel 2806 . . . . . . . . . . . 12 𝑚 𝑋𝐷
6968, 20nfan 1868 . . . . . . . . . . 11 𝑚(𝑋𝐷𝑛𝑍)
7029adantl 481 . . . . . . . . . . 11 ((𝑋𝐷𝑛𝑍) → 𝑛 ∈ ℤ)
7133a1i 11 . . . . . . . . . . 11 ((𝑋𝐷𝑛𝑍) → 𝑍 ∈ V)
7236adantl 481 . . . . . . . . . . 11 ((𝑋𝐷𝑛𝑍) → (ℤ𝑛) ⊆ 𝑍)
73 fvexd 6241 . . . . . . . . . . 11 (((𝑋𝐷𝑛𝑍) ∧ 𝑚𝑍) → ((𝐹𝑚)‘𝑋) ∈ V)
74 fvexd 6241 . . . . . . . . . . 11 ((𝑋𝐷𝑛𝑍) → (ℤ𝑛) ∈ V)
75 ssid 3657 . . . . . . . . . . . 12 (ℤ𝑛) ⊆ (ℤ𝑛)
7675a1i 11 . . . . . . . . . . 11 ((𝑋𝐷𝑛𝑍) → (ℤ𝑛) ⊆ (ℤ𝑛))
77 fvexd 6241 . . . . . . . . . . 11 (((𝑋𝐷𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝐹𝑚)‘𝑋) ∈ V)
78 eqidd 2652 . . . . . . . . . . 11 (((𝑋𝐷𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝐹𝑚)‘𝑋) = ((𝐹𝑚)‘𝑋))
7969, 70, 31, 71, 72, 73, 74, 76, 77, 78climeldmeqmpt 40218 . . . . . . . . . 10 ((𝑋𝐷𝑛𝑍) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ ↔ (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ ))
8059, 79mpbid 222 . . . . . . . . 9 ((𝑋𝐷𝑛𝑍) → (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ )
81 climdm 14329 . . . . . . . . 9 ((𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) ∈ dom ⇝ ↔ (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) ⇝ ( ⇝ ‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))))
8280, 81sylib 208 . . . . . . . 8 ((𝑋𝐷𝑛𝑍) → (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) ⇝ ( ⇝ ‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))))
831, 82sylan 487 . . . . . . 7 ((𝜑𝑛𝑍) → (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) ⇝ ( ⇝ ‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))))
84833adant3 1101 . . . . . 6 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) ⇝ ( ⇝ ‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))))
85 simpl1 1084 . . . . . . 7 (((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝜑)
86 simpl2 1085 . . . . . . 7 (((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑛𝑍)
87 nfcv 2793 . . . . . . . . . . . . 13 𝑗dom (𝐹𝑚)
88 fnlimfvre.m . . . . . . . . . . . . . . 15 𝑚𝐹
89 nfcv 2793 . . . . . . . . . . . . . . 15 𝑚𝑗
9088, 89nffv 6236 . . . . . . . . . . . . . 14 𝑚(𝐹𝑗)
9190nfdm 5399 . . . . . . . . . . . . 13 𝑚dom (𝐹𝑗)
92 fveq2 6229 . . . . . . . . . . . . . 14 (𝑚 = 𝑗 → (𝐹𝑚) = (𝐹𝑗))
9392dmeqd 5358 . . . . . . . . . . . . 13 (𝑚 = 𝑗 → dom (𝐹𝑚) = dom (𝐹𝑗))
9487, 91, 93cbviin 4590 . . . . . . . . . . . 12 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑗 ∈ (ℤ𝑛)dom (𝐹𝑗)
9594eleq2i 2722 . . . . . . . . . . 11 (𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ↔ 𝑋 𝑗 ∈ (ℤ𝑛)dom (𝐹𝑗))
9695biimpi 206 . . . . . . . . . 10 (𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → 𝑋 𝑗 ∈ (ℤ𝑛)dom (𝐹𝑗))
9796adantr 480 . . . . . . . . 9 ((𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑋 𝑗 ∈ (ℤ𝑛)dom (𝐹𝑗))
98 simpr 476 . . . . . . . . 9 ((𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑗 ∈ (ℤ𝑛))
99 eliinid 39608 . . . . . . . . 9 ((𝑋 𝑗 ∈ (ℤ𝑛)dom (𝐹𝑗) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑋 ∈ dom (𝐹𝑗))
10097, 98, 99syl2anc 694 . . . . . . . 8 ((𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑋 ∈ dom (𝐹𝑗))
1011003ad2antl3 1245 . . . . . . 7 (((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑋 ∈ dom (𝐹𝑗))
102 id 22 . . . . . . . . . 10 (𝑗 ∈ (ℤ𝑛) → 𝑗 ∈ (ℤ𝑛))
103 fvexd 6241 . . . . . . . . . 10 (𝑗 ∈ (ℤ𝑛) → ((𝐹𝑗)‘𝑋) ∈ V)
10490, 21nffv 6236 . . . . . . . . . . 11 𝑚((𝐹𝑗)‘𝑋)
10592fveq1d 6231 . . . . . . . . . . 11 (𝑚 = 𝑗 → ((𝐹𝑚)‘𝑋) = ((𝐹𝑗)‘𝑋))
106 eqid 2651 . . . . . . . . . . 11 (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) = (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))
10789, 104, 105, 106fvmptf 6340 . . . . . . . . . 10 ((𝑗 ∈ (ℤ𝑛) ∧ ((𝐹𝑗)‘𝑋) ∈ V) → ((𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))‘𝑗) = ((𝐹𝑗)‘𝑋))
108102, 103, 107syl2anc 694 . . . . . . . . 9 (𝑗 ∈ (ℤ𝑛) → ((𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))‘𝑗) = ((𝐹𝑗)‘𝑋))
109108adantl 481 . . . . . . . 8 (((𝜑𝑛𝑍𝑋 ∈ dom (𝐹𝑗)) ∧ 𝑗 ∈ (ℤ𝑛)) → ((𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))‘𝑗) = ((𝐹𝑗)‘𝑋))
110 simpll 805 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝜑)
11135adantll 750 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑗𝑍)
11219, 63nfan 1868 . . . . . . . . . . . . 13 𝑚(𝜑𝑗𝑍)
113 nfcv 2793 . . . . . . . . . . . . . 14 𝑚
11490, 91, 113nff 6079 . . . . . . . . . . . . 13 𝑚(𝐹𝑗):dom (𝐹𝑗)⟶ℝ
115112, 114nfim 1865 . . . . . . . . . . . 12 𝑚((𝜑𝑗𝑍) → (𝐹𝑗):dom (𝐹𝑗)⟶ℝ)
116 eleq1 2718 . . . . . . . . . . . . . 14 (𝑚 = 𝑗 → (𝑚𝑍𝑗𝑍))
117116anbi2d 740 . . . . . . . . . . . . 13 (𝑚 = 𝑗 → ((𝜑𝑚𝑍) ↔ (𝜑𝑗𝑍)))
11892, 93feq12d 6071 . . . . . . . . . . . . 13 (𝑚 = 𝑗 → ((𝐹𝑚):dom (𝐹𝑚)⟶ℝ ↔ (𝐹𝑗):dom (𝐹𝑗)⟶ℝ))
119117, 118imbi12d 333 . . . . . . . . . . . 12 (𝑚 = 𝑗 → (((𝜑𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ) ↔ ((𝜑𝑗𝑍) → (𝐹𝑗):dom (𝐹𝑗)⟶ℝ)))
120 fnlimfvre.f . . . . . . . . . . . 12 ((𝜑𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
121115, 119, 120chvar 2298 . . . . . . . . . . 11 ((𝜑𝑗𝑍) → (𝐹𝑗):dom (𝐹𝑗)⟶ℝ)
122110, 111, 121syl2anc 694 . . . . . . . . . 10 (((𝜑𝑛𝑍) ∧ 𝑗 ∈ (ℤ𝑛)) → (𝐹𝑗):dom (𝐹𝑗)⟶ℝ)
1231223adantl3 1239 . . . . . . . . 9 (((𝜑𝑛𝑍𝑋 ∈ dom (𝐹𝑗)) ∧ 𝑗 ∈ (ℤ𝑛)) → (𝐹𝑗):dom (𝐹𝑗)⟶ℝ)
124 simpl3 1086 . . . . . . . . 9 (((𝜑𝑛𝑍𝑋 ∈ dom (𝐹𝑗)) ∧ 𝑗 ∈ (ℤ𝑛)) → 𝑋 ∈ dom (𝐹𝑗))
125123, 124ffvelrnd 6400 . . . . . . . 8 (((𝜑𝑛𝑍𝑋 ∈ dom (𝐹𝑗)) ∧ 𝑗 ∈ (ℤ𝑛)) → ((𝐹𝑗)‘𝑋) ∈ ℝ)
126109, 125eqeltrd 2730 . . . . . . 7 (((𝜑𝑛𝑍𝑋 ∈ dom (𝐹𝑗)) ∧ 𝑗 ∈ (ℤ𝑛)) → ((𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))‘𝑗) ∈ ℝ)
12785, 86, 101, 40, 126syl31anc 1369 . . . . . 6 (((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑗 ∈ (ℤ𝑛)) → ((𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))‘𝑗) ∈ ℝ)
12831, 30, 84, 127climrecl 14358 . . . . 5 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → ( ⇝ ‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))) ∈ ℝ)
12944, 128eqeltrd 2730 . . . 4 ((𝜑𝑛𝑍𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))) ∈ ℝ)
1301293exp 1283 . . 3 (𝜑 → (𝑛𝑍 → (𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))) ∈ ℝ)))
13117, 18, 130rexlimd 3055 . 2 (𝜑 → (∃𝑛𝑍 𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))) ∈ ℝ))
13216, 131mpd 15 1 (𝜑 → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054   = wceq 1523  wnf 1748  wcel 2030  wnfc 2780  wrex 2942  {crab 2945  Vcvv 3231  wss 3607   ciun 4552   ciin 4553   class class class wbr 4685  cmpt 4762  dom cdm 5143  wf 5922  cfv 5926  cr 9973  cz 11415  cuz 11725  cli 14259
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-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-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-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-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-sup 8389  df-inf 8390  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-rp 11871  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
This theorem is referenced by:  fnlimfvre2  40227  fnlimf  40228  smflimlem4  41303  smflim  41306
  Copyright terms: Public domain W3C validator