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 ⊢Ⅎ_xA
frsucmpt.2 ⊢Ⅎ_xB
frsucmpt.3 ⊢Ⅎ_xD
frsucmpt.4 ⊢F=rec⁡x∈V⟼CA↾ω
frsucmpt.5 ⊢x=F⁡B→C=D
Assertion frsucmptn ⊢¬D∈V→F⁡suc⁡B=∅

Proof

Step Hyp Ref Expression
1 frsucmpt.1 ⊢Ⅎ_xA
2 frsucmpt.2 ⊢Ⅎ_xB
3 frsucmpt.3 ⊢Ⅎ_xD
4 frsucmpt.4 ⊢F=rec⁡x∈V⟼CA↾ω
5 frsucmpt.5 ⊢x=F⁡B→C=D
6 4 fveq1i ⊢F⁡suc⁡B=rec⁡x∈V⟼CA↾ω⁡suc⁡B
7 frfnom ⊢rec⁡x∈V⟼CA↾ωFnω
8 fndm ⊢rec⁡x∈V⟼CA↾ωFnω→dom⁡rec⁡x∈V⟼CA↾ω=ω
9 7 8 ax-mp ⊢dom⁡rec⁡x∈V⟼CA↾ω=ω
10 9 eleq2i ⊢suc⁡B∈dom⁡rec⁡x∈V⟼CA↾ω↔suc⁡B∈ω
11 peano2b ⊢B∈ω↔suc⁡B∈ω
12 frsuc ⊢B∈ω→rec⁡x∈V⟼CA↾ω⁡suc⁡B=x∈V⟼C⁡rec⁡x∈V⟼CA↾ω⁡B
13 4 fveq1i ⊢F⁡B=rec⁡x∈V⟼CA↾ω⁡B
14 13 fveq2i ⊢x∈V⟼C⁡F⁡B=x∈V⟼C⁡rec⁡x∈V⟼CA↾ω⁡B
15 12 14 eqtr4di ⊢B∈ω→rec⁡x∈V⟼CA↾ω⁡suc⁡B=x∈V⟼C⁡F⁡B
16 nfmpt1 ⊢Ⅎ_xx∈V⟼C
17 16 1 nfrdg ⊢Ⅎ_xrec⁡x∈V⟼CA
18 nfcv ⊢Ⅎ_xω
19 17 18 nfres ⊢Ⅎ_xrec⁡x∈V⟼CA↾ω
20 4 19 nfcxfr ⊢Ⅎ_xF
21 20 2 nffv ⊢Ⅎ_xF⁡B
22 eqid ⊢x∈V⟼C=x∈V⟼C
23 21 3 5 22 fvmptnf ⊢¬D∈V→x∈V⟼C⁡F⁡B=∅
24 15 23 sylan9eqr ⊢¬D∈V∧B∈ω→rec⁡x∈V⟼CA↾ω⁡suc⁡B=∅
25 24 ex ⊢¬D∈V→B∈ω→rec⁡x∈V⟼CA↾ω⁡suc⁡B=∅
26 11 25 biimtrrid ⊢¬D∈V→suc⁡B∈ω→rec⁡x∈V⟼CA↾ω⁡suc⁡B=∅
27 10 26 biimtrid ⊢¬D∈V→suc⁡B∈dom⁡rec⁡x∈V⟼CA↾ω→rec⁡x∈V⟼CA↾ω⁡suc⁡B=∅
28 ndmfv ⊢¬suc⁡B∈dom⁡rec⁡x∈V⟼CA↾ω→rec⁡x∈V⟼CA↾ω⁡suc⁡B=∅
29 27 28 pm2.61d1 ⊢¬D∈V→rec⁡x∈V⟼CA↾ω⁡suc⁡B=∅
30 6 29 eqtrid ⊢¬D∈V→F⁡suc⁡B=∅