Step | Hyp | Ref
| Expression |
1 | | seqof2.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | seqof2.2 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
3 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑥(𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) |
4 | | nffvmpt1 6111 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) |
5 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑥𝐴 |
6 | | nffvmpt1 6111 |
. . . . . . . 8
⊢
Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛) |
7 | 5, 6 | nfmpt 4674 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) |
8 | 4, 7 | nfeq 2762 |
. . . . . 6
⊢
Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) |
9 | 3, 8 | nfim 1813 |
. . . . 5
⊢
Ⅎ𝑥((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛))) |
10 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑛 ∈ (𝑀...𝑁))) |
11 | 10 | anbi2d 736 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)))) |
12 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛)) |
13 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) |
14 | 13 | mpteq2dv 4673 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥)) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛))) |
15 | 12, 14 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥)) ↔ ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)))) |
16 | 11, 15 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = 𝑛 → (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥))) ↔ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛))))) |
17 | | seqof2.3 |
. . . . . . . 8
⊢ (𝜑 → (𝑀...𝑁) ⊆ 𝐵) |
18 | 17 | sselda 3568 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ 𝐵) |
19 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐴 ∈ 𝑉) |
20 | | mptexg 6389 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝑧 ∈ 𝐴 ↦ 𝑋) ∈ V) |
21 | 19, 20 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑧 ∈ 𝐴 ↦ 𝑋) ∈ V) |
22 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)) = (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)) |
23 | 22 | fvmpt2 6200 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ (𝑧 ∈ 𝐴 ↦ 𝑋) ∈ V) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = (𝑧 ∈ 𝐴 ↦ 𝑋)) |
24 | 18, 21, 23 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = (𝑧 ∈ 𝐴 ↦ 𝑋)) |
25 | 18 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ 𝑧 ∈ 𝐴) → 𝑥 ∈ 𝐵) |
26 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ 𝑧 ∈ 𝐴) → 𝜑) |
27 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
28 | | seqof2.4 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴)) → 𝑋 ∈ 𝑊) |
29 | 26, 25, 27, 28 | syl12anc 1316 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ 𝑧 ∈ 𝐴) → 𝑋 ∈ 𝑊) |
30 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 ↦ 𝑋) = (𝑥 ∈ 𝐵 ↦ 𝑋) |
31 | 30 | fvmpt2 6200 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝑊) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = 𝑋) |
32 | 25, 29, 31 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = 𝑋) |
33 | 32 | mpteq2dva 4672 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥)) = (𝑧 ∈ 𝐴 ↦ 𝑋)) |
34 | 24, 33 | eqtr4d 2647 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥))) |
35 | 9, 16, 34 | chvar 2250 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛))) |
36 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑦((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛) |
37 | | nfcsb1v 3515 |
. . . . . 6
⊢
Ⅎ𝑧⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋) |
38 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑧𝑛 |
39 | 37, 38 | nffv 6110 |
. . . . 5
⊢
Ⅎ𝑧(⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛) |
40 | | csbeq1a 3508 |
. . . . . 6
⊢ (𝑧 = 𝑦 → (𝑥 ∈ 𝐵 ↦ 𝑋) = ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)) |
41 | 40 | fveq1d 6105 |
. . . . 5
⊢ (𝑧 = 𝑦 → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛) = (⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) |
42 | 36, 39, 41 | cbvmpt 4677 |
. . . 4
⊢ (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) = (𝑦 ∈ 𝐴 ↦ (⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) |
43 | 35, 42 | syl6eq 2660 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑦 ∈ 𝐴 ↦ (⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛))) |
44 | 1, 2, 43 | seqof 12720 |
. 2
⊢ (𝜑 → (seq𝑀( ∘𝑓 + , (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)))‘𝑁) = (𝑦 ∈ 𝐴 ↦ (seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁))) |
45 | | nfcv 2751 |
. . 3
⊢
Ⅎ𝑦(seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁) |
46 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑧𝑀 |
47 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑧
+ |
48 | 46, 47, 37 | nfseq 12673 |
. . . 4
⊢
Ⅎ𝑧seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)) |
49 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑧𝑁 |
50 | 48, 49 | nffv 6110 |
. . 3
⊢
Ⅎ𝑧(seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁) |
51 | 40 | seqeq3d 12671 |
. . . 4
⊢ (𝑧 = 𝑦 → seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋)) = seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋))) |
52 | 51 | fveq1d 6105 |
. . 3
⊢ (𝑧 = 𝑦 → (seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁) = (seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁)) |
53 | 45, 50, 52 | cbvmpt 4677 |
. 2
⊢ (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁)) = (𝑦 ∈ 𝐴 ↦ (seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁)) |
54 | 44, 53 | syl6eqr 2662 |
1
⊢ (𝜑 → (seq𝑀( ∘𝑓 + , (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)))‘𝑁) = (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁))) |