Step |
Hyp |
Ref |
Expression |
1 |
|
fnlimfvre2.p |
⊢ Ⅎ 𝑚 𝜑 |
2 |
|
fnlimfvre2.m |
⊢ Ⅎ 𝑚 𝐹 |
3 |
|
fnlimfvre2.n |
⊢ Ⅎ 𝑥 𝐹 |
4 |
|
fnlimfvre2.z |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
5 |
|
fnlimfvre2.f |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ ) |
6 |
|
fnlimfvre2.d |
⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } |
7 |
|
fnlimfvre2.g |
⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) |
8 |
|
fnlimfvre2.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐷 ) |
9 |
|
nfrab1 |
⊢ Ⅎ 𝑥 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } |
10 |
6 9
|
nfcxfr |
⊢ Ⅎ 𝑥 𝐷 |
11 |
|
nfcv |
⊢ Ⅎ 𝑧 𝐷 |
12 |
|
nfcv |
⊢ Ⅎ 𝑧 ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) |
13 |
|
nfcv |
⊢ Ⅎ 𝑥 ⇝ |
14 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑍 |
15 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑚 |
16 |
3 15
|
nffv |
⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑚 ) |
17 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑧 |
18 |
16 17
|
nffv |
⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) |
19 |
14 18
|
nfmpt |
⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) |
20 |
13 19
|
nffv |
⊢ Ⅎ 𝑥 ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) |
21 |
|
fveq2 |
⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) |
22 |
21
|
mpteq2dv |
⊢ ( 𝑥 = 𝑧 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) |
23 |
22
|
fveq2d |
⊢ ( 𝑥 = 𝑧 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) ) |
24 |
10 11 12 20 23
|
cbvmptf |
⊢ ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑧 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) ) |
25 |
7 24
|
eqtri |
⊢ 𝐺 = ( 𝑧 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) ) |
26 |
|
fveq2 |
⊢ ( 𝑋 = 𝑧 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) |
27 |
26
|
mpteq2dv |
⊢ ( 𝑋 = 𝑧 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) |
28 |
|
eqcom |
⊢ ( 𝑋 = 𝑧 ↔ 𝑧 = 𝑋 ) |
29 |
28
|
imbi1i |
⊢ ( ( 𝑋 = 𝑧 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) ↔ ( 𝑧 = 𝑋 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) ) |
30 |
|
eqcom |
⊢ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ↔ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) |
31 |
30
|
imbi2i |
⊢ ( ( 𝑧 = 𝑋 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) ↔ ( 𝑧 = 𝑋 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ) |
32 |
29 31
|
bitri |
⊢ ( ( 𝑋 = 𝑧 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) ↔ ( 𝑧 = 𝑋 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ) |
33 |
27 32
|
mpbi |
⊢ ( 𝑧 = 𝑋 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) |
34 |
33
|
fveq2d |
⊢ ( 𝑧 = 𝑋 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ) |
35 |
|
fvexd |
⊢ ( 𝜑 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ∈ V ) |
36 |
25 34 8 35
|
fvmptd3 |
⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ) |
37 |
1 2 3 4 5 6 8
|
fnlimfvre |
⊢ ( 𝜑 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ ) |
38 |
36 37
|
eqeltrd |
⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ ℝ ) |