Metamath Proof Explorer


Theorem rdgsucmptnf

Description: The value of the recursive definition generator at a successor (special case where the characteristic function is an ordered-pair class abstraction and where the mapping class D is a proper class). This is a technical lemma that can be used together with rdgsucmptf to help eliminate redundant sethood antecedents. (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 rdgsucmptnf
|- ( -. D e. _V -> ( F ` suc B ) = (/) )

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 4 fveq1i
 |-  ( F ` suc B ) = ( rec ( ( x e. _V |-> C ) , A ) ` suc B )
7 rdgdmlim
 |-  Lim dom rec ( ( x e. _V |-> C ) , A )
8 limsuc
 |-  ( Lim dom rec ( ( x e. _V |-> C ) , A ) -> ( B e. dom rec ( ( x e. _V |-> C ) , A ) <-> suc B e. dom rec ( ( x e. _V |-> C ) , A ) ) )
9 7 8 ax-mp
 |-  ( B e. dom rec ( ( x e. _V |-> C ) , A ) <-> suc B e. dom rec ( ( x e. _V |-> C ) , A ) )
10 rdgsucg
 |-  ( B e. dom rec ( ( x e. _V |-> C ) , A ) -> ( rec ( ( x e. _V |-> C ) , A ) ` suc B ) = ( ( x e. _V |-> C ) ` ( rec ( ( x e. _V |-> C ) , A ) ` B ) ) )
11 4 fveq1i
 |-  ( F ` B ) = ( rec ( ( x e. _V |-> C ) , A ) ` B )
12 11 fveq2i
 |-  ( ( x e. _V |-> C ) ` ( F ` B ) ) = ( ( x e. _V |-> C ) ` ( rec ( ( x e. _V |-> C ) , A ) ` B ) )
13 10 12 eqtr4di
 |-  ( B e. dom rec ( ( x e. _V |-> C ) , A ) -> ( rec ( ( x e. _V |-> C ) , A ) ` suc B ) = ( ( x e. _V |-> C ) ` ( F ` B ) ) )
14 nfmpt1
 |-  F/_ x ( x e. _V |-> C )
15 14 1 nfrdg
 |-  F/_ x rec ( ( x e. _V |-> C ) , A )
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 fvmptnf
 |-  ( -. D e. _V -> ( ( x e. _V |-> C ) ` ( F ` B ) ) = (/) )
20 13 19 sylan9eqr
 |-  ( ( -. D e. _V /\ B e. dom rec ( ( x e. _V |-> C ) , A ) ) -> ( rec ( ( x e. _V |-> C ) , A ) ` suc B ) = (/) )
21 20 ex
 |-  ( -. D e. _V -> ( B e. dom rec ( ( x e. _V |-> C ) , A ) -> ( rec ( ( x e. _V |-> C ) , A ) ` suc B ) = (/) ) )
22 9 21 syl5bir
 |-  ( -. D e. _V -> ( suc B e. dom rec ( ( x e. _V |-> C ) , A ) -> ( rec ( ( x e. _V |-> C ) , A ) ` suc B ) = (/) ) )
23 ndmfv
 |-  ( -. suc B e. dom rec ( ( x e. _V |-> C ) , A ) -> ( rec ( ( x e. _V |-> C ) , A ) ` suc B ) = (/) )
24 22 23 pm2.61d1
 |-  ( -. D e. _V -> ( rec ( ( x e. _V |-> C ) , A ) ` suc B ) = (/) )
25 6 24 eqtrid
 |-  ( -. D e. _V -> ( F ` suc B ) = (/) )