This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )