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