Step |
Hyp |
Ref |
Expression |
1 |
|
climresmpt.z |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
2 |
|
climresmpt.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) |
3 |
|
climresmpt.n |
⊢ ( 𝜑 → 𝑁 ∈ 𝑍 ) |
4 |
|
climresmpt.g |
⊢ 𝐺 = ( 𝑥 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ 𝐴 ) |
5 |
2
|
reseq1i |
⊢ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑁 ) ) = ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) |
6 |
5
|
a1i |
⊢ ( 𝜑 → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑁 ) ) = ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) ) |
7 |
3 1
|
eleqtrdi |
⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
8 |
|
uzss |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) ) |
9 |
7 8
|
syl |
⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) ) |
10 |
9 1
|
sseqtrrdi |
⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) ⊆ 𝑍 ) |
11 |
|
resmpt |
⊢ ( ( ℤ≥ ‘ 𝑁 ) ⊆ 𝑍 → ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) = ( 𝑥 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ 𝐴 ) ) |
12 |
10 11
|
syl |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) = ( 𝑥 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ 𝐴 ) ) |
13 |
4
|
eqcomi |
⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ 𝐴 ) = 𝐺 |
14 |
13
|
a1i |
⊢ ( 𝜑 → ( 𝑥 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ 𝐴 ) = 𝐺 ) |
15 |
6 12 14
|
3eqtrrd |
⊢ ( 𝜑 → 𝐺 = ( 𝐹 ↾ ( ℤ≥ ‘ 𝑁 ) ) ) |
16 |
15
|
breq1d |
⊢ ( 𝜑 → ( 𝐺 ⇝ 𝐵 ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑁 ) ) ⇝ 𝐵 ) ) |
17 |
|
eluzelz |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ ) |
18 |
7 17
|
syl |
⊢ ( 𝜑 → 𝑁 ∈ ℤ ) |
19 |
1
|
fvexi |
⊢ 𝑍 ∈ V |
20 |
19
|
mptex |
⊢ ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ∈ V |
21 |
20
|
a1i |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ∈ V ) |
22 |
2 21
|
eqeltrid |
⊢ ( 𝜑 → 𝐹 ∈ V ) |
23 |
|
climres |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐹 ∈ V ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑁 ) ) ⇝ 𝐵 ↔ 𝐹 ⇝ 𝐵 ) ) |
24 |
18 22 23
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑁 ) ) ⇝ 𝐵 ↔ 𝐹 ⇝ 𝐵 ) ) |
25 |
16 24
|
bitrd |
⊢ ( 𝜑 → ( 𝐺 ⇝ 𝐵 ↔ 𝐹 ⇝ 𝐵 ) ) |