Step | Hyp | Ref
| Expression |
1 | | fnlimfv.3 |
. . . 4
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
2 | | fnlimfv.1 |
. . . . 5
⊢
Ⅎ𝑥𝐷 |
3 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑦𝐷 |
4 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑦(
⇝ ‘(𝑚 ∈
𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) |
5 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑥
⇝ |
6 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥𝑍 |
7 | | fnlimfv.2 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝐹 |
8 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑚 |
9 | 7, 8 | nffv 6110 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝐹‘𝑚) |
10 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑦 |
11 | 9, 10 | nffv 6110 |
. . . . . . 7
⊢
Ⅎ𝑥((𝐹‘𝑚)‘𝑦) |
12 | 6, 11 | nfmpt 4674 |
. . . . . 6
⊢
Ⅎ𝑥(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) |
13 | 5, 12 | nffv 6110 |
. . . . 5
⊢
Ⅎ𝑥(
⇝ ‘(𝑚 ∈
𝑍 ↦ ((𝐹‘𝑚)‘𝑦))) |
14 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑚)‘𝑦)) |
15 | 14 | mpteq2dv 4673 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦))) |
16 | 15 | fveq2d 6107 |
. . . . 5
⊢ (𝑥 = 𝑦 → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)))) |
17 | 2, 3, 4, 13, 16 | cbvmptf 4676 |
. . . 4
⊢ (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) = (𝑦 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)))) |
18 | 1, 17 | eqtri 2632 |
. . 3
⊢ 𝐺 = (𝑦 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)))) |
19 | 18 | a1i 11 |
. 2
⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦))))) |
20 | | fveq2 6103 |
. . . . 5
⊢ (𝑦 = 𝑋 → ((𝐹‘𝑚)‘𝑦) = ((𝐹‘𝑚)‘𝑋)) |
21 | 20 | mpteq2dv 4673 |
. . . 4
⊢ (𝑦 = 𝑋 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) |
22 | 21 | fveq2d 6107 |
. . 3
⊢ (𝑦 = 𝑋 → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦))) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)))) |
23 | 22 | adantl 481 |
. 2
⊢ ((𝜑 ∧ 𝑦 = 𝑋) → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦))) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)))) |
24 | | fnlimfv.4 |
. 2
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
25 | | fvex 6113 |
. . 3
⊢ ( ⇝
‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) ∈ V |
26 | 25 | a1i 11 |
. 2
⊢ (𝜑 → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) ∈ V) |
27 | 19, 23, 24, 26 | fvmptd 6197 |
1
⊢ (𝜑 → (𝐺‘𝑋) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)))) |