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

Metamath Proof Explorer

Theorem frsucmpt2

Description: The successor value resulting from finite recursive definition generation (special case where the generation function is expressed in maps-to notation), using double-substitution instead of a bound variable condition. (Contributed by Mario Carneiro, 11-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 frsucmpt2.1 ⊢ 𝐹 = ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω )
2 frsucmpt2.2 ⊢ ( 𝑦 = 𝑥 → 𝐸 = 𝐶 )
3 frsucmpt2.3 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝐵 ) → 𝐸 = 𝐷 )
4 nfcv ⊢ Ⅎ 𝑦 𝐴
5 nfcv ⊢ Ⅎ 𝑦 𝐵
6 nfcv ⊢ Ⅎ 𝑦 𝐷
7 2 cbvmptv ⊢ ( 𝑦 ∈ V ↦ 𝐸 ) = ( 𝑥 ∈ V ↦ 𝐶 )
8 rdgeq1 ⊢ ( ( 𝑦 ∈ V ↦ 𝐸 ) = ( 𝑥 ∈ V ↦ 𝐶 ) → rec ( ( 𝑦 ∈ V ↦ 𝐸 ) , 𝐴 ) = rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) )
9 7 8 ax-mp ⊢ rec ( ( 𝑦 ∈ V ↦ 𝐸 ) , 𝐴 ) = rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 )
10 9 reseq1i ⊢ ( rec ( ( 𝑦 ∈ V ↦ 𝐸 ) , 𝐴 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω )
11 1 10 eqtr4i ⊢ 𝐹 = ( rec ( ( 𝑦 ∈ V ↦ 𝐸 ) , 𝐴 ) ↾ ω )
12 4 5 6 11 3 frsucmpt ⊢ ( ( 𝐵 ∈ ω ∧ 𝐷 ∈ 𝑉 ) → ( 𝐹 ‘ suc 𝐵 ) = 𝐷 )