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

Metamath Proof Explorer

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 )