| Step | Hyp | Ref
| Expression |
| 1 | | seqof2.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 2 | | seqof2.2 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
| 3 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑥(𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) |
| 4 | | nffvmpt1 6917 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) |
| 5 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑥𝐴 |
| 6 | | nffvmpt1 6917 |
. . . . . . . 8
⊢
Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛) |
| 7 | 5, 6 | nfmpt 5249 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) |
| 8 | 4, 7 | nfeq 2919 |
. . . . . 6
⊢
Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) |
| 9 | 3, 8 | nfim 1896 |
. . . . 5
⊢
Ⅎ𝑥((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛))) |
| 10 | | eleq1w 2824 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑛 ∈ (𝑀...𝑁))) |
| 11 | 10 | anbi2d 630 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)))) |
| 12 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛)) |
| 13 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) |
| 14 | 13 | mpteq2dv 5244 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥)) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛))) |
| 15 | 12, 14 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥)) ↔ ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)))) |
| 16 | 11, 15 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = 𝑛 → (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥))) ↔ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛))))) |
| 17 | | seqof2.3 |
. . . . . . . 8
⊢ (𝜑 → (𝑀...𝑁) ⊆ 𝐵) |
| 18 | 17 | sselda 3983 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ 𝐵) |
| 19 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐴 ∈ 𝑉) |
| 20 | 19 | mptexd 7244 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑧 ∈ 𝐴 ↦ 𝑋) ∈ V) |
| 21 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)) = (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)) |
| 22 | 21 | fvmpt2 7027 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ (𝑧 ∈ 𝐴 ↦ 𝑋) ∈ V) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = (𝑧 ∈ 𝐴 ↦ 𝑋)) |
| 23 | 18, 20, 22 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = (𝑧 ∈ 𝐴 ↦ 𝑋)) |
| 24 | 18 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ 𝑧 ∈ 𝐴) → 𝑥 ∈ 𝐵) |
| 25 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ 𝑧 ∈ 𝐴) → 𝜑) |
| 26 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
| 27 | | seqof2.4 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴)) → 𝑋 ∈ 𝑊) |
| 28 | 25, 24, 26, 27 | syl12anc 837 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ 𝑧 ∈ 𝐴) → 𝑋 ∈ 𝑊) |
| 29 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 ↦ 𝑋) = (𝑥 ∈ 𝐵 ↦ 𝑋) |
| 30 | 29 | fvmpt2 7027 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝑊) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = 𝑋) |
| 31 | 24, 28, 30 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = 𝑋) |
| 32 | 31 | mpteq2dva 5242 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥)) = (𝑧 ∈ 𝐴 ↦ 𝑋)) |
| 33 | 23, 32 | eqtr4d 2780 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑥) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥))) |
| 34 | 9, 16, 33 | chvarfv 2240 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛))) |
| 35 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑦((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛) |
| 36 | | nfcsb1v 3923 |
. . . . . 6
⊢
Ⅎ𝑧⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋) |
| 37 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑧𝑛 |
| 38 | 36, 37 | nffv 6916 |
. . . . 5
⊢
Ⅎ𝑧(⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛) |
| 39 | | csbeq1a 3913 |
. . . . . 6
⊢ (𝑧 = 𝑦 → (𝑥 ∈ 𝐵 ↦ 𝑋) = ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)) |
| 40 | 39 | fveq1d 6908 |
. . . . 5
⊢ (𝑧 = 𝑦 → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛) = (⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) |
| 41 | 35, 38, 40 | cbvmpt 5253 |
. . . 4
⊢ (𝑧 ∈ 𝐴 ↦ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) = (𝑦 ∈ 𝐴 ↦ (⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛)) |
| 42 | 34, 41 | eqtrdi 2793 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → ((𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋))‘𝑛) = (𝑦 ∈ 𝐴 ↦ (⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑛))) |
| 43 | 1, 2, 42 | seqof 14100 |
. 2
⊢ (𝜑 → (seq𝑀( ∘f + , (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)))‘𝑁) = (𝑦 ∈ 𝐴 ↦ (seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁))) |
| 44 | | nfcv 2905 |
. . 3
⊢
Ⅎ𝑦(seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁) |
| 45 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑧𝑀 |
| 46 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑧
+ |
| 47 | 45, 46, 36 | nfseq 14052 |
. . . 4
⊢
Ⅎ𝑧seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋)) |
| 48 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑧𝑁 |
| 49 | 47, 48 | nffv 6916 |
. . 3
⊢
Ⅎ𝑧(seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁) |
| 50 | 39 | seqeq3d 14050 |
. . . 4
⊢ (𝑧 = 𝑦 → seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋)) = seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋))) |
| 51 | 50 | fveq1d 6908 |
. . 3
⊢ (𝑧 = 𝑦 → (seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁) = (seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁)) |
| 52 | 44, 49, 51 | cbvmpt 5253 |
. 2
⊢ (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁)) = (𝑦 ∈ 𝐴 ↦ (seq𝑀( + , ⦋𝑦 / 𝑧⦌(𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁)) |
| 53 | 43, 52 | eqtr4di 2795 |
1
⊢ (𝜑 → (seq𝑀( ∘f + , (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)))‘𝑁) = (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁))) |