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 _ x A
rdgsucmptf.2 _ x B
rdgsucmptf.3 _ x D
rdgsucmptf.4 F = rec x V C A
rdgsucmptf.5 x = F B C = D
Assertion rdgsucmptnf ¬ D V F suc B =

Proof

Step Hyp Ref Expression
1 rdgsucmptf.1 _ x A
2 rdgsucmptf.2 _ x B
3 rdgsucmptf.3 _ x D
4 rdgsucmptf.4 F = rec x V C A
5 rdgsucmptf.5 x = F B C = D
6 4 fveq1i F suc B = rec x V C A suc B
7 rdgdmlim Lim dom rec x V C A
8 limsuc Lim dom rec x V C A B dom rec x V C A suc B dom rec x V C A
9 7 8 ax-mp B dom rec x V C A suc B dom rec x V C A
10 rdgsucg B dom rec x V C A rec x V C A suc B = x V C rec x V C A B
11 4 fveq1i F B = rec x V C A B
12 11 fveq2i x V C F B = x V C rec x V C A B
13 10 12 eqtr4di B dom rec x V C A rec x V C A suc B = x V C F B
14 nfmpt1 _ x x V C
15 14 1 nfrdg _ x rec x V C A
16 4 15 nfcxfr _ x F
17 16 2 nffv _ x F 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 C A rec x V C A suc B =
21 20 ex ¬ D V B dom rec x V C A rec x V C A suc B =
22 9 21 syl5bir ¬ D V suc B dom rec x V C A rec x V C A suc B =
23 ndmfv ¬ suc B dom rec x V C A rec x V C A suc B =
24 22 23 pm2.61d1 ¬ D V rec x V C A suc B =
25 6 24 eqtrid ¬ D V F suc B =