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 𝐵 ) = 𝐷 )