Theorem frsucmpt2

Description: The successor value resulting from finite recursive definition generation (special case where the generation function is expressed in maps-to notation), using double-substitution instead of a bound variable condition. (Contributed by Mario Carneiro, 11-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		frsucmpt2.1	|- F = ( rec ( ( x e. _V |-> C ) , A ) |` _om )
2		frsucmpt2.2	|- ( y = x -> E = C )
3		frsucmpt2.3	|- ( y = ( F ` B ) -> E = D )
4		nfcv	|- F/_ y A
5		nfcv	|- F/_ y B
6		nfcv	|- F/_ y D
7	2	cbvmptv	|- ( y e. _V |-> E ) = ( x e. _V |-> C )
8		rdgeq1	|- ( ( y e. _V |-> E ) = ( x e. _V |-> C ) -> rec ( ( y e. _V |-> E ) , A ) = rec ( ( x e. _V |-> C ) , A ) )
9	7 8	ax-mp	|- rec ( ( y e. _V |-> E ) , A ) = rec ( ( x e. _V |-> C ) , A )
10	9	reseq1i	|- ( rec ( ( y e. _V |-> E ) , A ) |` _om ) = ( rec ( ( x e. _V |-> C ) , A ) |` _om )
11	1 10	eqtr4i	|- F = ( rec ( ( y e. _V |-> E ) , A ) |` _om )
12	4 5 6 11 3	frsucmpt	|- ( ( B e. _om /\ D e. V ) -> ( F ` suc B ) = D )