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	$⊢ \underline{Ⅎ} x A$
		rdgsucmptf.2	$⊢ \underline{Ⅎ} x B$
		rdgsucmptf.3	$⊢ \underline{Ⅎ} x D$
		rdgsucmptf.4	$⊢ F = rec ((x \in V ⟼ C), A)$
		rdgsucmptf.5	$⊢ x = F (B) \to C = D$
	Assertion	rdgsucmptf	$⊢ (B \in On \land D \in V) \to F (suc B) = D$

Proof

Step	Hyp	Ref	Expression
1		rdgsucmptf.1	$⊢ \underline{Ⅎ} x A$
2		rdgsucmptf.2	$⊢ \underline{Ⅎ} x B$
3		rdgsucmptf.3	$⊢ \underline{Ⅎ} x D$
4		rdgsucmptf.4	$⊢ F = rec ((x \in V ⟼ C), A)$
5		rdgsucmptf.5	$⊢ x = F (B) \to C = D$
6		rdgsuc	$⊢ B \in On \to rec ((x \in V ⟼ C), A) (suc B) = (x \in V ⟼ C) (rec ((x \in V ⟼ C), A) (B))$
7	4	fveq1i	$⊢ F (suc B) = rec ((x \in V ⟼ C), A) (suc B)$
8	4	fveq1i	$⊢ F (B) = rec ((x \in V ⟼ C), A) (B)$
9	8	fveq2i	$⊢ (x \in V ⟼ C) (F (B)) = (x \in V ⟼ C) (rec ((x \in V ⟼ C), A) (B))$
10	6 7 9	3eqtr4g	$⊢ B \in On \to F (suc B) = (x \in V ⟼ C) (F (B))$
11		fvex	$⊢ F (B) \in V$
12		nfmpt1	$⊢ \underline{Ⅎ} x (x \in V ⟼ C)$
13	12 1	nfrdg	$⊢ \underline{Ⅎ} x rec ((x \in V ⟼ C), A)$
14	4 13	nfcxfr	$⊢ \underline{Ⅎ} x F$
15	14 2	nffv	$⊢ \underline{Ⅎ} x F (B)$
16		eqid	$⊢ (x \in V ⟼ C) = (x \in V ⟼ C)$
17	15 3 5 16	fvmptf	$⊢ (F (B) \in V \land D \in V) \to (x \in V ⟼ C) (F (B)) = D$
18	11 17	mpan	$⊢ D \in V \to (x \in V ⟼ C) (F (B)) = D$
19	10 18	sylan9eq	$⊢ (B \in On \land D \in V) \to F (suc B) = D$