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 𝑥 𝐴
rdgsucmptf.2 𝑥 𝐵
rdgsucmptf.3 𝑥 𝐷
rdgsucmptf.4 𝐹 = rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 )
rdgsucmptf.5 ( 𝑥 = ( 𝐹𝐵 ) → 𝐶 = 𝐷 )
Assertion rdgsucmptnf ( ¬ 𝐷 ∈ V → ( 𝐹 ‘ suc 𝐵 ) = ∅ )

Proof

Step Hyp Ref Expression
1 rdgsucmptf.1 𝑥 𝐴
2 rdgsucmptf.2 𝑥 𝐵
3 rdgsucmptf.3 𝑥 𝐷
4 rdgsucmptf.4 𝐹 = rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 )
5 rdgsucmptf.5 ( 𝑥 = ( 𝐹𝐵 ) → 𝐶 = 𝐷 )
6 4 fveq1i ( 𝐹 ‘ suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ‘ suc 𝐵 )
7 rdgdmlim Lim dom rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 )
8 limsuc ( Lim dom rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) → ( 𝐵 ∈ dom rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↔ suc 𝐵 ∈ dom rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ) )
9 7 8 ax-mp ( 𝐵 ∈ dom rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↔ suc 𝐵 ∈ dom rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) )
10 rdgsucg ( 𝐵 ∈ dom rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) → ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ‘ 𝐵 ) ) )
11 4 fveq1i ( 𝐹𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ‘ 𝐵 )
12 11 fveq2i ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( 𝐹𝐵 ) ) = ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ‘ 𝐵 ) )
13 10 12 eqtr4di ( 𝐵 ∈ dom rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) → ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( 𝐹𝐵 ) ) )
14 nfmpt1 𝑥 ( 𝑥 ∈ V ↦ 𝐶 )
15 14 1 nfrdg 𝑥 rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 )
16 4 15 nfcxfr 𝑥 𝐹
17 16 2 nffv 𝑥 ( 𝐹𝐵 )
18 eqid ( 𝑥 ∈ V ↦ 𝐶 ) = ( 𝑥 ∈ V ↦ 𝐶 )
19 17 3 5 18 fvmptnf ( ¬ 𝐷 ∈ V → ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( 𝐹𝐵 ) ) = ∅ )
20 13 19 sylan9eqr ( ( ¬ 𝐷 ∈ V ∧ 𝐵 ∈ dom rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ) → ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ‘ suc 𝐵 ) = ∅ )
21 20 ex ( ¬ 𝐷 ∈ V → ( 𝐵 ∈ dom rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) → ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ‘ suc 𝐵 ) = ∅ ) )
22 9 21 syl5bir ( ¬ 𝐷 ∈ V → ( suc 𝐵 ∈ dom rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) → ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ‘ suc 𝐵 ) = ∅ ) )
23 ndmfv ( ¬ suc 𝐵 ∈ dom rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) → ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ‘ suc 𝐵 ) = ∅ )
24 22 23 pm2.61d1 ( ¬ 𝐷 ∈ V → ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ‘ suc 𝐵 ) = ∅ )
25 6 24 eqtrid ( ¬ 𝐷 ∈ V → ( 𝐹 ‘ suc 𝐵 ) = ∅ )