Theorem frsucmpt

Description: The successor value resulting from finite recursive definition generation (special case where the generation function is expressed in maps-to notation). (Contributed by NM, 14-Sep-2003) (Revised by Scott Fenton, 2-Nov-2011)

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

Proof

Step	Hyp	Ref	Expression
1		frsucmpt.1	|- F/_ x A
2		frsucmpt.2	|- F/_ x B
3		frsucmpt.3	|- F/_ x D
4		frsucmpt.4	|- F = ( rec ( ( x e. _V |-> C ) , A ) |` _om )
5		frsucmpt.5	|- ( x = ( F ` B ) -> C = D )
6		frsuc	|- ( B e. _om -> ( ( rec ( ( x e. _V |-> C ) , A ) |` _om ) ` suc B ) = ( ( x e. _V |-> C ) ` ( ( rec ( ( x e. _V |-> C ) , A ) |` _om ) ` B ) ) )
7	4	fveq1i	|- ( F ` suc B ) = ( ( rec ( ( x e. _V |-> C ) , A ) |` _om ) ` suc B )
8	4	fveq1i	|- ( F ` B ) = ( ( rec ( ( x e. _V |-> C ) , A ) |` _om ) ` B )
9	8	fveq2i	|- ( ( x e. _V |-> C ) ` ( F ` B ) ) = ( ( x e. _V |-> C ) ` ( ( rec ( ( x e. _V |-> C ) , A ) |` _om ) ` B ) )
10	6 7 9	3eqtr4g	|- ( B e. _om -> ( 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		nfcv	|- F/_ x _om
15	13 14	nfres	|- F/_ x ( rec ( ( x e. _V |-> C ) , A ) |` _om )
16	4 15	nfcxfr	|- F/_ x F
17	16 2	nffv	|- F/_ x ( F ` B )
18		eqid	|- ( x e. _V |-> C ) = ( x e. _V |-> C )
19	17 3 5 18	fvmptf	|- ( ( ( F ` B ) e. _V /\ D e. V ) -> ( ( x e. _V |-> C ) ` ( F ` B ) ) = D )
20	11 19	mpan	|- ( D e. V -> ( ( x e. _V |-> C ) ` ( F ` B ) ) = D )
21	10 20	sylan9eq	|- ( ( B e. _om /\ D e. V ) -> ( F ` suc B ) = D )