Step |
Hyp |
Ref |
Expression |
0 |
|
cF |
⊢ 𝐹 |
1 |
|
cI |
⊢ 𝐼 |
2 |
0 1
|
cseqom |
⊢ seqω ( 𝐹 , 𝐼 ) |
3 |
|
vi |
⊢ 𝑖 |
4 |
|
com |
⊢ ω |
5 |
|
vv |
⊢ 𝑣 |
6 |
|
cvv |
⊢ V |
7 |
3
|
cv |
⊢ 𝑖 |
8 |
7
|
csuc |
⊢ suc 𝑖 |
9 |
5
|
cv |
⊢ 𝑣 |
10 |
7 9 0
|
co |
⊢ ( 𝑖 𝐹 𝑣 ) |
11 |
8 10
|
cop |
⊢ 〈 suc 𝑖 , ( 𝑖 𝐹 𝑣 ) 〉 |
12 |
3 5 4 6 11
|
cmpo |
⊢ ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ 〈 suc 𝑖 , ( 𝑖 𝐹 𝑣 ) 〉 ) |
13 |
|
c0 |
⊢ ∅ |
14 |
|
cid |
⊢ I |
15 |
1 14
|
cfv |
⊢ ( I ‘ 𝐼 ) |
16 |
13 15
|
cop |
⊢ 〈 ∅ , ( I ‘ 𝐼 ) 〉 |
17 |
12 16
|
crdg |
⊢ rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ 〈 suc 𝑖 , ( 𝑖 𝐹 𝑣 ) 〉 ) , 〈 ∅ , ( I ‘ 𝐼 ) 〉 ) |
18 |
17 4
|
cima |
⊢ ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ 〈 suc 𝑖 , ( 𝑖 𝐹 𝑣 ) 〉 ) , 〈 ∅ , ( I ‘ 𝐼 ) 〉 ) “ ω ) |
19 |
2 18
|
wceq |
⊢ seqω ( 𝐹 , 𝐼 ) = ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ 〈 suc 𝑖 , ( 𝑖 𝐹 𝑣 ) 〉 ) , 〈 ∅ , ( I ‘ 𝐼 ) 〉 ) “ ω ) |