Step |
Hyp |
Ref |
Expression |
1 |
|
fnlimfv.1 |
⊢ Ⅎ 𝑥 𝐷 |
2 |
|
fnlimfv.2 |
⊢ Ⅎ 𝑥 𝐹 |
3 |
|
fnlimfv.3 |
⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) |
4 |
|
fnlimfv.4 |
⊢ ( 𝜑 → 𝑋 ∈ 𝐷 ) |
5 |
|
nfcv |
⊢ Ⅎ 𝑦 𝐷 |
6 |
|
nfcv |
⊢ Ⅎ 𝑦 ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) |
7 |
|
nfcv |
⊢ Ⅎ 𝑥 ⇝ |
8 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑍 |
9 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑚 |
10 |
2 9
|
nffv |
⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑚 ) |
11 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑦 |
12 |
10 11
|
nffv |
⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) |
13 |
8 12
|
nfmpt |
⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) |
14 |
7 13
|
nffv |
⊢ Ⅎ 𝑥 ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) |
15 |
|
fveq2 |
⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) |
16 |
15
|
mpteq2dv |
⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) |
17 |
16
|
fveq2d |
⊢ ( 𝑥 = 𝑦 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) ) |
18 |
1 5 6 14 17
|
cbvmptf |
⊢ ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) ) |
19 |
3 18
|
eqtri |
⊢ 𝐺 = ( 𝑦 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) ) |
20 |
|
fveq2 |
⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) |
21 |
20
|
mpteq2dv |
⊢ ( 𝑦 = 𝑋 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) |
22 |
21
|
fveq2d |
⊢ ( 𝑦 = 𝑋 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ) |
23 |
|
fvexd |
⊢ ( 𝜑 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ∈ V ) |
24 |
19 22 4 23
|
fvmptd3 |
⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ) |