frsucmpt

Description: The successor value resulting from finite recursive definition generation (special case where the generation function is expressed in maps-to notation). (Contributed by NM, 14-Sep-2003) (Revised by Scott Fenton, 2-Nov-2011)

	Ref	Expression
Hypotheses	frsucmpt.1	$⊢ \underline{Ⅎ} x A$
	frsucmpt.2	$⊢ \underline{Ⅎ} x B$
	frsucmpt.3	$⊢ \underline{Ⅎ} x D$
	frsucmpt.4	$⊢ F = {rec ((x \in V ⟼ C), A) ↾}_{ω}$
	frsucmpt.5	$⊢ x = F (B) \to C = D$
Assertion	frsucmpt	$⊢ (B \in ω \land D \in V) \to F (suc B) = D$

Proof

Step	Hyp	Ref	Expression
1		frsucmpt.1	$⊢ \underline{Ⅎ} x A$
2		frsucmpt.2	$⊢ \underline{Ⅎ} x B$
3		frsucmpt.3	$⊢ \underline{Ⅎ} x D$
4		frsucmpt.4	$⊢ F = {rec ((x \in V ⟼ C), A) ↾}_{ω}$
5		frsucmpt.5	$⊢ x = F (B) \to C = D$
6		frsuc	$⊢ B \in ω \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 ω \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		nfcv	$⊢ \underline{Ⅎ} x ω$
15	13 14	nfres	$⊢ \underline{Ⅎ} x ({rec ((x \in V ⟼ C), A) ↾}_{ω})$
16	4 15	nfcxfr	$⊢ \underline{Ⅎ} x F$
17	16 2	nffv	$⊢ \underline{Ⅎ} x F (B)$
18		eqid	$⊢ (x \in V ⟼ C) = (x \in V ⟼ C)$
19	17 3 5 18	fvmptf	$⊢ (F (B) \in V \land D \in V) \to (x \in V ⟼ C) (F (B)) = D$
20	11 19	mpan	$⊢ D \in V \to (x \in V ⟼ C) (F (B)) = D$
21	10 20	sylan9eq	$⊢ (B \in ω \land D \in V) \to F (suc B) = D$

Metamath Proof Explorer

Theorem frsucmpt

Proof