Step |
Hyp |
Ref |
Expression |
1 |
|
nfseq.1 |
⊢ Ⅎ 𝑥 𝑀 |
2 |
|
nfseq.2 |
⊢ Ⅎ 𝑥 + |
3 |
|
nfseq.3 |
⊢ Ⅎ 𝑥 𝐹 |
4 |
|
df-seq |
⊢ seq 𝑀 ( + , 𝐹 ) = ( rec ( ( 𝑧 ∈ V , 𝑤 ∈ V ↦ 〈 ( 𝑧 + 1 ) , ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) 〉 ) , 〈 𝑀 , ( 𝐹 ‘ 𝑀 ) 〉 ) “ ω ) |
5 |
|
nfcv |
⊢ Ⅎ 𝑥 V |
6 |
|
nfcv |
⊢ Ⅎ 𝑥 ( 𝑧 + 1 ) |
7 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑤 |
8 |
3 6
|
nffv |
⊢ Ⅎ 𝑥 ( 𝐹 ‘ ( 𝑧 + 1 ) ) |
9 |
7 2 8
|
nfov |
⊢ Ⅎ 𝑥 ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) |
10 |
6 9
|
nfop |
⊢ Ⅎ 𝑥 〈 ( 𝑧 + 1 ) , ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) 〉 |
11 |
5 5 10
|
nfmpo |
⊢ Ⅎ 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ 〈 ( 𝑧 + 1 ) , ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) 〉 ) |
12 |
3 1
|
nffv |
⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑀 ) |
13 |
1 12
|
nfop |
⊢ Ⅎ 𝑥 〈 𝑀 , ( 𝐹 ‘ 𝑀 ) 〉 |
14 |
11 13
|
nfrdg |
⊢ Ⅎ 𝑥 rec ( ( 𝑧 ∈ V , 𝑤 ∈ V ↦ 〈 ( 𝑧 + 1 ) , ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) 〉 ) , 〈 𝑀 , ( 𝐹 ‘ 𝑀 ) 〉 ) |
15 |
|
nfcv |
⊢ Ⅎ 𝑥 ω |
16 |
14 15
|
nfima |
⊢ Ⅎ 𝑥 ( rec ( ( 𝑧 ∈ V , 𝑤 ∈ V ↦ 〈 ( 𝑧 + 1 ) , ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) 〉 ) , 〈 𝑀 , ( 𝐹 ‘ 𝑀 ) 〉 ) “ ω ) |
17 |
4 16
|
nfcxfr |
⊢ Ⅎ 𝑥 seq 𝑀 ( + , 𝐹 ) |