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

Metamath Proof Explorer

Theorem rdgsucmptf

Description: The value of the recursive definition generator at a successor (special case where the characteristic function uses the map operation). (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 rdgsucmptf ( ( 𝐵 ∈ On ∧ 𝐷 ∈ 𝑉 ) → ( 𝐹 ‘ suc 𝐵 ) = 𝐷 )

Proof

Step Hyp Ref Expression
1 rdgsucmptf.1 ⊢ Ⅎ 𝑥 𝐴
2 rdgsucmptf.2 ⊢ Ⅎ 𝑥 𝐵
3 rdgsucmptf.3 ⊢ Ⅎ 𝑥 𝐷
4 rdgsucmptf.4 ⊢ 𝐹 = rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 )
5 rdgsucmptf.5 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝐵 ) → 𝐶 = 𝐷 )
6 rdgsuc ⊢ ( 𝐵 ∈ On → ( 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 ⊢ ( 𝐵 ∈ On → ( 𝐹 ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( 𝐹 ‘ 𝐵 ) ) )
11 fvex ⊢ ( 𝐹 ‘ 𝐵 ) ∈ V
12 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ V ↦ 𝐶 )
13 12 1 nfrdg ⊢ Ⅎ 𝑥 rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 )
14 4 13 nfcxfr ⊢ Ⅎ 𝑥 𝐹
15 14 2 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝐵 )
16 eqid ⊢ ( 𝑥 ∈ V ↦ 𝐶 ) = ( 𝑥 ∈ V ↦ 𝐶 )
17 15 3 5 16 fvmptf ⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ V ∧ 𝐷 ∈ 𝑉 ) → ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( 𝐹 ‘ 𝐵 ) ) = 𝐷 )
18 11 17 mpan ⊢ ( 𝐷 ∈ 𝑉 → ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( 𝐹 ‘ 𝐵 ) ) = 𝐷 )
19 10 18 sylan9eq ⊢ ( ( 𝐵 ∈ On ∧ 𝐷 ∈ 𝑉 ) → ( 𝐹 ‘ suc 𝐵 ) = 𝐷 )