Step | Hyp | Ref
| Expression |
1 | | seqof2.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | seqof2.2 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
3 | | nfv 1922 |
. . . . . 6
⊢
Ⅎ𝑥(𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) |
4 | | nffvmpt1 6749 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) |
5 | | nfcv 2906 |
. . . . . . . 8
⊢
Ⅎ𝑥𝐴 |
6 | | nffvmpt1 6749 |
. . . . . . . 8
⊢
Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛) |
7 | 5, 6 | nfmpt 5168 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) |
8 | 4, 7 | nfeq 2919 |
. . . . . 6
⊢
Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) |
9 | 3, 8 | nfim 1904 |
. . . . 5
⊢
Ⅎ𝑥((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛))) |
10 | | eleq1w 2822 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑛 ∈ (𝑀...𝑁))) |
11 | 10 | anbi2d 632 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)))) |
12 | | fveq2 6738 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛)) |
13 | | fveq2 6738 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) |
14 | 13 | mpteq2dv 5167 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥)) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛))) |
15 | 12, 14 | eqeq12d 2755 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥)) ↔ ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)))) |
16 | 11, 15 | imbi12d 348 |
. . . . 5
⊢ (𝑥 = 𝑛 → (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥))) ↔ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛))))) |
17 | | seqof2.3 |
. . . . . . . 8
⊢ (𝜑 → (𝑀...𝑁) ⊆ 𝐵) |
18 | 17 | sselda 3917 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ 𝐵) |
19 | 1 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐴 ∈ 𝑉) |
20 | 19 | mptexd 7061 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑧 ∈ 𝐴 ↦ 𝑋) ∈ V) |
21 | | eqid 2739 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)) = (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)) |
22 | 21 | fvmpt2 6850 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ (𝑧 ∈ 𝐴 ↦ 𝑋) ∈ V) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = (𝑧 ∈ 𝐴 ↦ 𝑋)) |
23 | 18, 20, 22 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = (𝑧 ∈ 𝐴 ↦ 𝑋)) |
24 | 18 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ 𝑧 ∈ 𝐴) → 𝑥 ∈ 𝐵) |
25 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ 𝑧 ∈ 𝐴) → 𝜑) |
26 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
27 | | seqof2.4 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴)) → 𝑋 ∈ 𝑊) |
28 | 25, 24, 26, 27 | syl12anc 837 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ 𝑧 ∈ 𝐴) → 𝑋 ∈ 𝑊) |
29 | | eqid 2739 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 ↦ 𝑋) = (𝑥 ∈ 𝐵 ↦ 𝑋) |
30 | 29 | fvmpt2 6850 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝑊) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = 𝑋) |
31 | 24, 28, 30 | syl2anc 587 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = 𝑋) |
32 | 31 | mpteq2dva 5166 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥)) = (𝑧 ∈ 𝐴 ↦ 𝑋)) |
33 | 23, 32 | eqtr4d 2782 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥))) |
34 | 9, 16, 33 | chvarfv 2240 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛))) |
35 | | nfcv 2906 |
. . . . 5
⊢
Ⅎ𝑦((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛) |
36 | | nfcsb1v 3852 |
. . . . . 6
⊢
Ⅎ𝑧⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋) |
37 | | nfcv 2906 |
. . . . . 6
⊢
Ⅎ𝑧𝑛 |
38 | 36, 37 | nffv 6748 |
. . . . 5
⊢
Ⅎ𝑧(⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛) |
39 | | csbeq1a 3841 |
. . . . . 6
⊢ (𝑧 = 𝑦 → (𝑥 ∈ 𝐵 ↦ 𝑋) = ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)) |
40 | 39 | fveq1d 6740 |
. . . . 5
⊢ (𝑧 = 𝑦 → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛) = (⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) |
41 | 35, 38, 40 | cbvmpt 5172 |
. . . 4
⊢ (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) = (𝑦 ∈ 𝐴 ↦ (⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) |
42 | 34, 41 | eqtrdi 2796 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑦 ∈ 𝐴 ↦ (⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛))) |
43 | 1, 2, 42 | seqof 13662 |
. 2
⊢ (𝜑 → (seq𝑀( ∘f + , (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)))‘𝑁) = (𝑦 ∈ 𝐴 ↦ (seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁))) |
44 | | nfcv 2906 |
. . 3
⊢
Ⅎ𝑦(seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁) |
45 | | nfcv 2906 |
. . . . 5
⊢
Ⅎ𝑧𝑀 |
46 | | nfcv 2906 |
. . . . 5
⊢
Ⅎ𝑧
+ |
47 | 45, 46, 36 | nfseq 13613 |
. . . 4
⊢
Ⅎ𝑧seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)) |
48 | | nfcv 2906 |
. . . 4
⊢
Ⅎ𝑧𝑁 |
49 | 47, 48 | nffv 6748 |
. . 3
⊢
Ⅎ𝑧(seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁) |
50 | 39 | seqeq3d 13611 |
. . . 4
⊢ (𝑧 = 𝑦 → seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋)) = seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋))) |
51 | 50 | fveq1d 6740 |
. . 3
⊢ (𝑧 = 𝑦 → (seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁) = (seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁)) |
52 | 44, 49, 51 | cbvmpt 5172 |
. 2
⊢ (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁)) = (𝑦 ∈ 𝐴 ↦ (seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁)) |
53 | 43, 52 | eqtr4di 2798 |
1
⊢ (𝜑 → (seq𝑀( ∘f + , (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)))‘𝑁) = (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁))) |