Step |
Hyp |
Ref |
Expression |
1 |
|
findreccl.1 |
|- ( z e. P -> ( G ` z ) e. P ) |
2 |
|
rdg0g |
|- ( A e. P -> ( rec ( G , A ) ` (/) ) = A ) |
3 |
|
eleq1a |
|- ( A e. P -> ( ( rec ( G , A ) ` (/) ) = A -> ( rec ( G , A ) ` (/) ) e. P ) ) |
4 |
2 3
|
mpd |
|- ( A e. P -> ( rec ( G , A ) ` (/) ) e. P ) |
5 |
|
nnon |
|- ( y e. _om -> y e. On ) |
6 |
|
fveq2 |
|- ( z = ( rec ( G , A ) ` y ) -> ( G ` z ) = ( G ` ( rec ( G , A ) ` y ) ) ) |
7 |
6
|
eleq1d |
|- ( z = ( rec ( G , A ) ` y ) -> ( ( G ` z ) e. P <-> ( G ` ( rec ( G , A ) ` y ) ) e. P ) ) |
8 |
7 1
|
vtoclga |
|- ( ( rec ( G , A ) ` y ) e. P -> ( G ` ( rec ( G , A ) ` y ) ) e. P ) |
9 |
|
rdgsuc |
|- ( y e. On -> ( rec ( G , A ) ` suc y ) = ( G ` ( rec ( G , A ) ` y ) ) ) |
10 |
9
|
eleq1d |
|- ( y e. On -> ( ( rec ( G , A ) ` suc y ) e. P <-> ( G ` ( rec ( G , A ) ` y ) ) e. P ) ) |
11 |
8 10
|
syl5ibr |
|- ( y e. On -> ( ( rec ( G , A ) ` y ) e. P -> ( rec ( G , A ) ` suc y ) e. P ) ) |
12 |
5 11
|
syl |
|- ( y e. _om -> ( ( rec ( G , A ) ` y ) e. P -> ( rec ( G , A ) ` suc y ) e. P ) ) |
13 |
12
|
a1d |
|- ( y e. _om -> ( A e. P -> ( ( rec ( G , A ) ` y ) e. P -> ( rec ( G , A ) ` suc y ) e. P ) ) ) |
14 |
4 13
|
findfvcl |
|- ( C e. _om -> ( A e. P -> ( rec ( G , A ) ` C ) e. P ) ) |