Theorem rdgsucmptf 7151

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
rdgsucmptf	|- ( ( B e. On /\ D e. V ) -> ( F ` suc B ) = D )

Proof of Theorem rdgsucmptf

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

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1446   e. wcel 1889   F/_wnfc 2581   _Vcvv 3047   |-> cmpt 4464   Oncon0 5426   suc csuc 5428   ` cfv 5585   reccrdg 7132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-reu 2746  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-wrecs 7033  df-recs 7095  df-rdg 7133

This theorem is referenced by:  rdgsucmpt2  7153  rdgsucmpt  7154