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

Proof

Step Hyp Ref Expression
1 rdgsucmptf.1 ⊢Ⅎ_xA
2 rdgsucmptf.2 ⊢Ⅎ_xB
3 rdgsucmptf.3 ⊢Ⅎ_xD
4 rdgsucmptf.4 ⊢F=rec⁡x∈V⟼CA
5 rdgsucmptf.5 ⊢x=F⁡B→C=D
6 4 fveq1i ⊢F⁡suc⁡B=rec⁡x∈V⟼CA⁡suc⁡B
7 rdgdmlim ⊢Lim⁡dom⁡rec⁡x∈V⟼CA
8 limsuc ⊢Lim⁡dom⁡rec⁡x∈V⟼CA→B∈dom⁡rec⁡x∈V⟼CA↔suc⁡B∈dom⁡rec⁡x∈V⟼CA
9 7 8 ax-mp ⊢B∈dom⁡rec⁡x∈V⟼CA↔suc⁡B∈dom⁡rec⁡x∈V⟼CA
10 rdgsucg ⊢B∈dom⁡rec⁡x∈V⟼CA→rec⁡x∈V⟼CA⁡suc⁡B=x∈V⟼C⁡rec⁡x∈V⟼CA⁡B
11 4 fveq1i ⊢F⁡B=rec⁡x∈V⟼CA⁡B
12 11 fveq2i ⊢x∈V⟼C⁡F⁡B=x∈V⟼C⁡rec⁡x∈V⟼CA⁡B
13 10 12 eqtr4di ⊢B∈dom⁡rec⁡x∈V⟼CA→rec⁡x∈V⟼CA⁡suc⁡B=x∈V⟼C⁡F⁡B
14 nfmpt1 ⊢Ⅎ_xx∈V⟼C
15 14 1 nfrdg ⊢Ⅎ_xrec⁡x∈V⟼CA
16 4 15 nfcxfr ⊢Ⅎ_xF
17 16 2 nffv ⊢Ⅎ_xF⁡B
18 eqid ⊢x∈V⟼C=x∈V⟼C
19 17 3 5 18 fvmptnf ⊢¬D∈V→x∈V⟼C⁡F⁡B=∅
20 13 19 sylan9eqr ⊢¬D∈V∧B∈dom⁡rec⁡x∈V⟼CA→rec⁡x∈V⟼CA⁡suc⁡B=∅
21 20 ex ⊢¬D∈V→B∈dom⁡rec⁡x∈V⟼CA→rec⁡x∈V⟼CA⁡suc⁡B=∅
22 9 21 biimtrrid ⊢¬D∈V→suc⁡B∈dom⁡rec⁡x∈V⟼CA→rec⁡x∈V⟼CA⁡suc⁡B=∅
23 ndmfv ⊢¬suc⁡B∈dom⁡rec⁡x∈V⟼CA→rec⁡x∈V⟼CA⁡suc⁡B=∅
24 22 23 pm2.61d1 ⊢¬D∈V→rec⁡x∈V⟼CA⁡suc⁡B=∅
25 6 24 eqtrid ⊢¬D∈V→F⁡suc⁡B=∅