This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rdg0

Description: The initial value of the recursive definition generator. (Contributed by NM, 23-Apr-1995) (Revised by Mario Carneiro, 14-Nov-2014)

Ref Expression
Hypothesis rdg.1 
|- A e. _V
Assertion rdg0 
|- ( rec ( F , A ) ` (/) ) = A

Proof

Step Hyp Ref Expression
1 rdg.1 
 |-  A e. _V
2 rdgdmlim 
 |-  Lim dom rec ( F , A )
3 limomss 
 |-  ( Lim dom rec ( F , A ) -> _om C_ dom rec ( F , A ) )
4 2 3 ax-mp 
 |-  _om C_ dom rec ( F , A )
5 peano1 
 |-  (/) e. _om
6 4 5 sselii 
 |-  (/) e. dom rec ( F , A )
7 eqid 
 |-  ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) ) = ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) )
8 rdgvalg 
 |-  ( y e. dom rec ( F , A ) -> ( rec ( F , A ) ` y ) = ( ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) ) ` ( rec ( F , A ) |` y ) ) )
9 7 8 1 tz7.44-1 
 |-  ( (/) e. dom rec ( F , A ) -> ( rec ( F , A ) ` (/) ) = A )
10 6 9 ax-mp 
 |-  ( rec ( F , A ) ` (/) ) = A