Metamath Proof Explorer

Theorem frsucmpt

Description: The successor value resulting from finite recursive definition generation (special case where the generation function is expressed in maps-to notation). (Contributed by NM, 14-Sep-2003) (Revised by Scott Fenton, 2-Nov-2011)

Ref Expression
Hypotheses frsucmpt.1 ⊢ Ⅎ 𝑥 𝐴
frsucmpt.2 ⊢ Ⅎ 𝑥 𝐵
frsucmpt.3 ⊢ Ⅎ 𝑥 𝐷
frsucmpt.4 ⊢ 𝐹 = ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω )
frsucmpt.5 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝐵 ) → 𝐶 = 𝐷 )
Assertion frsucmpt ( ( 𝐵 ∈ ω ∧ 𝐷 ∈ 𝑉 ) → ( 𝐹 ‘ suc 𝐵 ) = 𝐷 )

Proof

Step Hyp Ref Expression
1 frsucmpt.1 ⊢ Ⅎ 𝑥 𝐴
2 frsucmpt.2 ⊢ Ⅎ 𝑥 𝐵
3 frsucmpt.3 ⊢ Ⅎ 𝑥 𝐷
4 frsucmpt.4 ⊢ 𝐹 = ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω )
5 frsucmpt.5 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝐵 ) → 𝐶 = 𝐷 )
6 frsuc ⊢ ( 𝐵 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ) )
7 4 fveq1i ⊢ ( 𝐹 ‘ suc 𝐵 ) = ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 )
8 4 fveq1i ⊢ ( 𝐹 ‘ 𝐵 ) = ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 )
9 8 fveq2i ⊢ ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( 𝐹 ‘ 𝐵 ) ) = ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) )
10 6 7 9 3eqtr4g ⊢ ( 𝐵 ∈ ω → ( 𝐹 ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( 𝐹 ‘ 𝐵 ) ) )
11 fvex ⊢ ( 𝐹 ‘ 𝐵 ) ∈ V
12 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ V ↦ 𝐶 )
13 12 1 nfrdg ⊢ Ⅎ 𝑥 rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 )
14 nfcv ⊢ Ⅎ 𝑥 ω
15 13 14 nfres ⊢ Ⅎ 𝑥 ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω )
16 4 15 nfcxfr ⊢ Ⅎ 𝑥 𝐹
17 16 2 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝐵 )
18 eqid ⊢ ( 𝑥 ∈ V ↦ 𝐶 ) = ( 𝑥 ∈ V ↦ 𝐶 )
19 17 3 5 18 fvmptf ⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ V ∧ 𝐷 ∈ 𝑉 ) → ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( 𝐹 ‘ 𝐵 ) ) = 𝐷 )
20 11 19 mpan ⊢ ( 𝐷 ∈ 𝑉 → ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( 𝐹 ‘ 𝐵 ) ) = 𝐷 )
21 10 20 sylan9eq ⊢ ( ( 𝐵 ∈ ω ∧ 𝐷 ∈ 𝑉 ) → ( 𝐹 ‘ suc 𝐵 ) = 𝐷 )