Step |
Hyp |
Ref |
Expression |
0 |
|
cF |
|- F |
1 |
|
cI |
|- I |
2 |
0 1
|
cseqom |
|- seqom ( F , I ) |
3 |
|
vi |
|- i |
4 |
|
com |
|- _om |
5 |
|
vv |
|- v |
6 |
|
cvv |
|- _V |
7 |
3
|
cv |
|- i |
8 |
7
|
csuc |
|- suc i |
9 |
5
|
cv |
|- v |
10 |
7 9 0
|
co |
|- ( i F v ) |
11 |
8 10
|
cop |
|- <. suc i , ( i F v ) >. |
12 |
3 5 4 6 11
|
cmpo |
|- ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) |
13 |
|
c0 |
|- (/) |
14 |
|
cid |
|- _I |
15 |
1 14
|
cfv |
|- ( _I ` I ) |
16 |
13 15
|
cop |
|- <. (/) , ( _I ` I ) >. |
17 |
12 16
|
crdg |
|- rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |
18 |
17 4
|
cima |
|- ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) " _om ) |
19 |
2 18
|
wceq |
|- seqom ( F , I ) = ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) " _om ) |