Theorem rdgsucmptf

Description: The value of the recursive definition generator at a successor (special case where the characteristic function uses the map operation). (Contributed by NM, 22-Oct-2003) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	rdgsucmptf.1	|- F/_ x A
	rdgsucmptf.2	|- F/_ x B
	rdgsucmptf.3	|- F/_ x D
	rdgsucmptf.4	|- F = rec ( ( x e. _V |-> C ) , A )
	rdgsucmptf.5	|- ( x = ( F ` B ) -> C = D )
Assertion	rdgsucmptf	|- ( ( B e. On /\ D e. V ) -> ( F ` suc B ) = D )

Proof

Step	Hyp	Ref	Expression
1		rdgsucmptf.1	|- F/_ x A
2		rdgsucmptf.2	|- F/_ x B
3		rdgsucmptf.3	|- F/_ x D
4		rdgsucmptf.4	|- F = rec ( ( x e. _V |-> C ) , A )
5		rdgsucmptf.5	|- ( x = ( F ` B ) -> C = D )
6		rdgsuc	|- ( B e. On -> ( rec ( ( x e. _V |-> C ) , A ) ` suc B ) = ( ( x e. _V |-> C ) ` ( rec ( ( x e. _V |-> C ) , A ) ` B ) ) )
7	4	fveq1i	|- ( F ` suc B ) = ( rec ( ( x e. _V |-> C ) , A ) ` suc B )
8	4	fveq1i	|- ( F ` B ) = ( rec ( ( x e. _V |-> C ) , A ) ` B )
9	8	fveq2i	|- ( ( x e. _V |-> C ) ` ( F ` B ) ) = ( ( x e. _V |-> C ) ` ( rec ( ( x e. _V |-> C ) , A ) ` B ) )
10	6 7 9	3eqtr4g	|- ( B e. On -> ( F ` suc B ) = ( ( x e. _V |-> C ) ` ( F ` B ) ) )
11		fvex	|- ( F ` B ) e. _V
12		nfmpt1	|- F/_ x ( x e. _V |-> C )
13	12 1	nfrdg	|- F/_ x rec ( ( x e. _V |-> C ) , A )
14	4 13	nfcxfr	|- F/_ x F
15	14 2	nffv	|- F/_ x ( F ` B )
16		eqid	|- ( x e. _V |-> C ) = ( x e. _V |-> C )
17	15 3 5 16	fvmptf	|- ( ( ( F ` B ) e. _V /\ D e. V ) -> ( ( x e. _V |-> C ) ` ( F ` B ) ) = D )
18	11 17	mpan	|- ( D e. V -> ( ( x e. _V |-> C ) ` ( F ` B ) ) = D )
19	10 18	sylan9eq	|- ( ( B e. On /\ D e. V ) -> ( F ` suc B ) = D )