Description: The value of the recursive definition generator at a successor (special case where the characteristic function uses the map operation). (Contributed by Mario Carneiro, 9-Sep-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rdgsucmpt.1 | ⊢ 𝐹 = rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) | |
rdgsucmpt.2 | ⊢ ( 𝑥 = ( 𝐹 ‘ 𝐵 ) → 𝐶 = 𝐷 ) | ||
Assertion | rdgsucmpt | ⊢ ( ( 𝐵 ∈ On ∧ 𝐷 ∈ 𝑉 ) → ( 𝐹 ‘ suc 𝐵 ) = 𝐷 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rdgsucmpt.1 | ⊢ 𝐹 = rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) | |
2 | rdgsucmpt.2 | ⊢ ( 𝑥 = ( 𝐹 ‘ 𝐵 ) → 𝐶 = 𝐷 ) | |
3 | nfcv | ⊢ Ⅎ 𝑥 𝐴 | |
4 | nfcv | ⊢ Ⅎ 𝑥 𝐵 | |
5 | nfcv | ⊢ Ⅎ 𝑥 𝐷 | |
6 | 3 4 5 1 2 | rdgsucmptf | ⊢ ( ( 𝐵 ∈ On ∧ 𝐷 ∈ 𝑉 ) → ( 𝐹 ‘ suc 𝐵 ) = 𝐷 ) |