Metamath Proof Explorer


Theorem findreccl

Description: Please add description here. (Contributed by Jeff Hoffman, 19-Feb-2008)

Ref Expression
Hypothesis findreccl.1
|- ( z e. P -> ( G ` z ) e. P )
Assertion findreccl
|- ( C e. _om -> ( A e. P -> ( rec ( G , A ) ` C ) e. P ) )

Proof

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 ) )