This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrrid ⊢ ( ¬ 𝐷 ∈ 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 𝐵 ) = ∅ )