Metamath Proof Explorer

Theorem frsucmptn

Description: The value of the finite recursive definition generator at a successor (special case where the characteristic function is a mapping abstraction and where the mapping class D is a proper class). This is a technical lemma that can be used together with frsucmpt to help eliminate redundant sethood antecedents. (Contributed by Scott Fenton, 19-Feb-2011) (Revised by Mario Carneiro, 11-Sep-2015)

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 frsucmptn 
|- ( -. D e. _V -> ( F ` suc B ) = (/) )

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 4 fveq1i 
 |-  ( F ` suc B ) = ( ( rec ( ( x e. _V |-> C ) , A ) |` _om ) ` suc B )
7 frfnom 
 |-  ( rec ( ( x e. _V |-> C ) , A ) |` _om ) Fn _om
8 fndm 
 |-  ( ( rec ( ( x e. _V |-> C ) , A ) |` _om ) Fn _om -> dom ( rec ( ( x e. _V |-> C ) , A ) |` _om ) = _om )
9 7 8 ax-mp 
 |-  dom ( rec ( ( x e. _V |-> C ) , A ) |` _om ) = _om
10 9 eleq2i 
 |-  ( suc B e. dom ( rec ( ( x e. _V |-> C ) , A ) |` _om ) <-> suc B e. _om )
11 peano2b 
 |-  ( B e. _om <-> suc B e. _om )
12 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 ) ) )
13 4 fveq1i 
 |-  ( F ` B ) = ( ( rec ( ( x e. _V |-> C ) , A ) |` _om ) ` B )
14 13 fveq2i 
 |-  ( ( x e. _V |-> C ) ` ( F ` B ) ) = ( ( x e. _V |-> C ) ` ( ( rec ( ( x e. _V |-> C ) , A ) |` _om ) ` B ) )
15 12 14 eqtr4di 
 |-  ( B e. _om -> ( ( rec ( ( x e. _V |-> C ) , A ) |` _om ) ` suc B ) = ( ( x e. _V |-> C ) ` ( F ` B ) ) )
16 nfmpt1 
 |-  F/_ x ( x e. _V |-> C )
17 16 1 nfrdg 
 |-  F/_ x rec ( ( x e. _V |-> C ) , A )
18 nfcv 
 |-  F/_ x _om
19 17 18 nfres 
 |-  F/_ x ( rec ( ( x e. _V |-> C ) , A ) |` _om )
20 4 19 nfcxfr 
 |-  F/_ x F
21 20 2 nffv 
 |-  F/_ x ( F ` B )
22 eqid 
 |-  ( x e. _V |-> C ) = ( x e. _V |-> C )
23 21 3 5 22 fvmptnf 
 |-  ( -. D e. _V -> ( ( x e. _V |-> C ) ` ( F ` B ) ) = (/) )
24 15 23 sylan9eqr 
 |-  ( ( -. D e. _V /\ B e. _om ) -> ( ( rec ( ( x e. _V |-> C ) , A ) |` _om ) ` suc B ) = (/) )
25 24 ex 
 |-  ( -. D e. _V -> ( B e. _om -> ( ( rec ( ( x e. _V |-> C ) , A ) |` _om ) ` suc B ) = (/) ) )
26 11 25 biimtrrid 
 |-  ( -. D e. _V -> ( suc B e. _om -> ( ( rec ( ( x e. _V |-> C ) , A ) |` _om ) ` suc B ) = (/) ) )
27 10 26 biimtrid 
 |-  ( -. D e. _V -> ( suc B e. dom ( rec ( ( x e. _V |-> C ) , A ) |` _om ) -> ( ( rec ( ( x e. _V |-> C ) , A ) |` _om ) ` suc B ) = (/) ) )
28 ndmfv 
 |-  ( -. suc B e. dom ( rec ( ( x e. _V |-> C ) , A ) |` _om ) -> ( ( rec ( ( x e. _V |-> C ) , A ) |` _om ) ` suc B ) = (/) )
29 27 28 pm2.61d1 
 |-  ( -. D e. _V -> ( ( rec ( ( x e. _V |-> C ) , A ) |` _om ) ` suc B ) = (/) )
30 6 29 eqtrid 
 |-  ( -. D e. _V -> ( F ` suc B ) = (/) )