Step |
Hyp |
Ref |
Expression |
1 |
|
2clim.1 |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
2 |
|
climmpt.2 |
⊢ 𝐺 = ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) |
3 |
|
simpr |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → 𝐹 ∈ 𝑉 ) |
4 |
|
fvex |
⊢ ( ℤ≥ ‘ 𝑀 ) ∈ V |
5 |
1 4
|
eqeltri |
⊢ 𝑍 ∈ V |
6 |
5
|
mptex |
⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ∈ V |
7 |
2 6
|
eqeltri |
⊢ 𝐺 ∈ V |
8 |
7
|
a1i |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → 𝐺 ∈ V ) |
9 |
|
simpl |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → 𝑀 ∈ ℤ ) |
10 |
|
fveq2 |
⊢ ( 𝑘 = 𝑚 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) ) |
11 |
|
fvex |
⊢ ( 𝐹 ‘ 𝑚 ) ∈ V |
12 |
10 2 11
|
fvmpt |
⊢ ( 𝑚 ∈ 𝑍 → ( 𝐺 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑚 ) ) |
13 |
12
|
eqcomd |
⊢ ( 𝑚 ∈ 𝑍 → ( 𝐹 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑚 ) ) |
14 |
13
|
adantl |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑚 ) ) |
15 |
1 3 8 9 14
|
climeq |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) ) |