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

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 biimtrrid 
 |-  ( -. 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 ) = (/) )