Step | Hyp | Ref
| Expression |
1 | | fnlimfvre.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
2 | | fnlimfvre.d |
. . . . . 6
⊢ 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } |
3 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑍 |
4 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑥(ℤ≥‘𝑛) |
5 | | fnlimfvre.n |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝐹 |
6 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑚 |
7 | 5, 6 | nffv 6110 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝐹‘𝑚) |
8 | 7 | nfdm 5288 |
. . . . . . . . 9
⊢
Ⅎ𝑥dom
(𝐹‘𝑚) |
9 | 4, 8 | nfiin 4485 |
. . . . . . . 8
⊢
Ⅎ𝑥∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
10 | 3, 9 | nfiun 4484 |
. . . . . . 7
⊢
Ⅎ𝑥∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
11 | 10 | ssrab2f 38331 |
. . . . . 6
⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
12 | 2, 11 | eqsstri 3598 |
. . . . 5
⊢ 𝐷 ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
13 | 12 | sseli 3564 |
. . . 4
⊢ (𝑋 ∈ 𝐷 → 𝑋 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) |
14 | | eliun 4460 |
. . . 4
⊢ (𝑋 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ↔ ∃𝑛 ∈ 𝑍 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) |
15 | 13, 14 | sylib 207 |
. . 3
⊢ (𝑋 ∈ 𝐷 → ∃𝑛 ∈ 𝑍 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) |
16 | 1, 15 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑛 ∈ 𝑍 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) |
17 | | nfv 1830 |
. . 3
⊢
Ⅎ𝑛𝜑 |
18 | | nfv 1830 |
. . 3
⊢
Ⅎ𝑛( ⇝
‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) ∈ ℝ |
19 | | fnlimfvre.p |
. . . . . . 7
⊢
Ⅎ𝑚𝜑 |
20 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑚 𝑛 ∈ 𝑍 |
21 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑚𝑋 |
22 | | nfii1 4487 |
. . . . . . . 8
⊢
Ⅎ𝑚∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
23 | 21, 22 | nfel 2763 |
. . . . . . 7
⊢
Ⅎ𝑚 𝑋 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) |
24 | 19, 20, 23 | nf3an 1819 |
. . . . . 6
⊢
Ⅎ𝑚(𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) |
25 | | uzssz 11583 |
. . . . . . . 8
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
26 | | fnlimfvre.z |
. . . . . . . . . 10
⊢ 𝑍 =
(ℤ≥‘𝑀) |
27 | 26 | eleq2i 2680 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (ℤ≥‘𝑀)) |
28 | 27 | biimpi 205 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑀)) |
29 | 25, 28 | sseldi 3566 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) |
30 | 29 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝑛 ∈ ℤ) |
31 | | eqid 2610 |
. . . . . 6
⊢
(ℤ≥‘𝑛) = (ℤ≥‘𝑛) |
32 | | fvex 6113 |
. . . . . . . 8
⊢
(ℤ≥‘𝑀) ∈ V |
33 | 26, 32 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑍 ∈ V |
34 | 33 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝑍 ∈ V) |
35 | 26 | uztrn2 11581 |
. . . . . . . 8
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑗 ∈ 𝑍) |
36 | 35 | ssd 38278 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑍 → (ℤ≥‘𝑛) ⊆ 𝑍) |
37 | 36 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → (ℤ≥‘𝑛) ⊆ 𝑍) |
38 | | fvex 6113 |
. . . . . . 7
⊢ ((𝐹‘𝑚)‘𝑋) ∈ V |
39 | 38 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ 𝑍) → ((𝐹‘𝑚)‘𝑋) ∈ V) |
40 | | fvex 6113 |
. . . . . . 7
⊢
(ℤ≥‘𝑛) ∈ V |
41 | 40 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → (ℤ≥‘𝑛) ∈ V) |
42 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑗 ∈ (ℤ≥‘𝑛)) |
43 | 42 | ssd 38278 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → (ℤ≥‘𝑛) ⊆
(ℤ≥‘𝑛)) |
44 | 38 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝐹‘𝑚)‘𝑋) ∈ V) |
45 | | eqidd 2611 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝐹‘𝑚)‘𝑋) = ((𝐹‘𝑚)‘𝑋)) |
46 | 24, 30, 31, 34, 37, 39, 41, 43, 44, 45 | climfveqmpt 38738 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) = ( ⇝ ‘(𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)))) |
47 | 2 | eleq2i 2680 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝐷 ↔ 𝑋 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }) |
48 | 47 | biimpi 205 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐷 → 𝑋 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }) |
49 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥𝑋 |
50 | 7, 49 | nffv 6110 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥((𝐹‘𝑚)‘𝑋) |
51 | 3, 50 | nfmpt 4674 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)) |
52 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥dom
⇝ |
53 | 51, 52 | nfel 2763 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)) ∈ dom ⇝ |
54 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑋 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑚)‘𝑋)) |
55 | 54 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑋 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) |
56 | 55 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑋 → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)) ∈ dom ⇝ )) |
57 | 49, 10, 53, 56 | elrabf 3329 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } ↔ (𝑋 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)) ∈ dom ⇝ )) |
58 | 57 | biimpi 205 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } → (𝑋 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)) ∈ dom ⇝ )) |
59 | 58 | simprd 478 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)) ∈ dom ⇝ ) |
60 | 48, 59 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝐷 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)) ∈ dom ⇝ ) |
61 | 60 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)) ∈ dom ⇝ ) |
62 | | nfmpt1 4675 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) |
63 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚dom
⇝ |
64 | 62, 63 | nfel 2763 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ |
65 | | nfv 1830 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚 𝑗 ∈ 𝑍 |
66 | 65 | nfci 2741 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚𝑍 |
67 | 66, 22 | nfiun 4484 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
68 | 64, 67 | nfrab 3100 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑚{𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } |
69 | 2, 68 | nfcxfr 2749 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑚𝐷 |
70 | 21, 69 | nfel 2763 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚 𝑋 ∈ 𝐷 |
71 | 70, 20 | nfan 1816 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚(𝑋 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) |
72 | 29 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ ℤ) |
73 | 33 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) → 𝑍 ∈ V) |
74 | 36 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) → (ℤ≥‘𝑛) ⊆ 𝑍) |
75 | 38 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ 𝑍) → ((𝐹‘𝑚)‘𝑋) ∈ V) |
76 | 40 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) → (ℤ≥‘𝑛) ∈ V) |
77 | | ssid 3587 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘𝑛) ⊆ (ℤ≥‘𝑛) |
78 | 77 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) → (ℤ≥‘𝑛) ⊆
(ℤ≥‘𝑛)) |
79 | 38 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝐹‘𝑚)‘𝑋) ∈ V) |
80 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝐹‘𝑚)‘𝑋) = ((𝐹‘𝑚)‘𝑋)) |
81 | 71, 72, 31, 73, 74, 75, 76, 78, 79, 80 | climeldmeqmpt 38735 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)) ∈ dom ⇝ ↔ (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)) ∈ dom ⇝ )) |
82 | 61, 81 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) → (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)) ∈ dom ⇝ ) |
83 | | climdm 14133 |
. . . . . . . . 9
⊢ ((𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)) ∈ dom ⇝ ↔ (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)) ⇝ ( ⇝ ‘(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)))) |
84 | 82, 83 | sylib 207 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) → (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)) ⇝ ( ⇝ ‘(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)))) |
85 | 1, 84 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)) ⇝ ( ⇝ ‘(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)))) |
86 | 85 | 3adant3 1074 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)) ⇝ ( ⇝ ‘(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)))) |
87 | | simpl1 1057 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝜑) |
88 | | simpl2 1058 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑛 ∈ 𝑍) |
89 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗dom
(𝐹‘𝑚) |
90 | | fnlimfvre.m |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚𝐹 |
91 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚𝑗 |
92 | 90, 91 | nffv 6110 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑚(𝐹‘𝑗) |
93 | 92 | nfdm 5288 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑚dom
(𝐹‘𝑗) |
94 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑗 → (𝐹‘𝑚) = (𝐹‘𝑗)) |
95 | 94 | dmeqd 5248 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑗 → dom (𝐹‘𝑚) = dom (𝐹‘𝑗)) |
96 | 89, 93, 95 | cbviin 4494 |
. . . . . . . . . . . 12
⊢ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∩ 𝑗 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑗) |
97 | 96 | eleq2i 2680 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ↔ 𝑋 ∈ ∩
𝑗 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑗)) |
98 | 97 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) → 𝑋 ∈ ∩
𝑗 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑗)) |
99 | 98 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑋 ∈ ∩
𝑗 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑗)) |
100 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑗 ∈ (ℤ≥‘𝑛)) |
101 | | eliinid 38325 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ∩ 𝑗 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑗) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑋 ∈ dom (𝐹‘𝑗)) |
102 | 99, 100, 101 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝑋 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑋 ∈ dom (𝐹‘𝑗)) |
103 | 102 | 3ad2antl3 1218 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑋 ∈ dom (𝐹‘𝑗)) |
104 | | id 22 |
. . . . . . . . . 10
⊢ (𝑗 ∈
(ℤ≥‘𝑛) → 𝑗 ∈ (ℤ≥‘𝑛)) |
105 | | fvex 6113 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑗)‘𝑋) ∈ V |
106 | 105 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑗 ∈
(ℤ≥‘𝑛) → ((𝐹‘𝑗)‘𝑋) ∈ V) |
107 | 92, 21 | nffv 6110 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚((𝐹‘𝑗)‘𝑋) |
108 | 94 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑗 → ((𝐹‘𝑚)‘𝑋) = ((𝐹‘𝑗)‘𝑋)) |
109 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)) = (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)) |
110 | 91, 107, 108, 109 | fvmptf 6209 |
. . . . . . . . . 10
⊢ ((𝑗 ∈
(ℤ≥‘𝑛) ∧ ((𝐹‘𝑗)‘𝑋) ∈ V) → ((𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋))‘𝑗) = ((𝐹‘𝑗)‘𝑋)) |
111 | 104, 106,
110 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝑗 ∈
(ℤ≥‘𝑛) → ((𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋))‘𝑗) = ((𝐹‘𝑗)‘𝑋)) |
112 | 111 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ dom (𝐹‘𝑗)) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → ((𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋))‘𝑗) = ((𝐹‘𝑗)‘𝑋)) |
113 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝜑) |
114 | 35 | adantll 746 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑗 ∈ 𝑍) |
115 | 19, 65 | nfan 1816 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑚(𝜑 ∧ 𝑗 ∈ 𝑍) |
116 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑚ℝ |
117 | 92, 93, 116 | nff 5954 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑚(𝐹‘𝑗):dom (𝐹‘𝑗)⟶ℝ |
118 | 115, 117 | nfim 1813 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗):dom (𝐹‘𝑗)⟶ℝ) |
119 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑗 → (𝑚 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍)) |
120 | 119 | anbi2d 736 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑗 → ((𝜑 ∧ 𝑚 ∈ 𝑍) ↔ (𝜑 ∧ 𝑗 ∈ 𝑍))) |
121 | 94, 95 | feq12d 5946 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑗 → ((𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ ↔ (𝐹‘𝑗):dom (𝐹‘𝑗)⟶ℝ)) |
122 | 120, 121 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑗 → (((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) ↔ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗):dom (𝐹‘𝑗)⟶ℝ))) |
123 | | fnlimfvre.f |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) |
124 | 118, 122,
123 | chvar 2250 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗):dom (𝐹‘𝑗)⟶ℝ) |
125 | 113, 114,
124 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑗):dom (𝐹‘𝑗)⟶ℝ) |
126 | 125 | 3adantl3 1212 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ dom (𝐹‘𝑗)) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑗):dom (𝐹‘𝑗)⟶ℝ) |
127 | | simpl3 1059 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ dom (𝐹‘𝑗)) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑋 ∈ dom (𝐹‘𝑗)) |
128 | 126, 127 | ffvelrnd 6268 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ dom (𝐹‘𝑗)) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → ((𝐹‘𝑗)‘𝑋) ∈ ℝ) |
129 | 112, 128 | eqeltrd 2688 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ dom (𝐹‘𝑗)) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → ((𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋))‘𝑗) ∈ ℝ) |
130 | 87, 88, 103, 42, 129 | syl31anc 1321 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → ((𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋))‘𝑗) ∈ ℝ) |
131 | 31, 30, 86, 130 | climrecl 14162 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → ( ⇝ ‘(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋))) ∈ ℝ) |
132 | 46, 131 | eqeltrd 2688 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) ∈ ℝ) |
133 | 132 | 3exp 1256 |
. . 3
⊢ (𝜑 → (𝑛 ∈ 𝑍 → (𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) ∈ ℝ))) |
134 | 17, 18, 133 | rexlimd 3008 |
. 2
⊢ (𝜑 → (∃𝑛 ∈ 𝑍 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) ∈ ℝ)) |
135 | 16, 134 | mpd 15 |
1
⊢ (𝜑 → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) ∈ ℝ) |