frsucmpt2

Description: The successor value resulting from finite recursive definition generation (special case where the generation function is expressed in maps-to notation), using double-substitution instead of a bound variable condition. (Contributed by Mario Carneiro, 11-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		frsucmpt2.1	$⊢ F = {rec ((x \in V ⟼ C), A) ↾}_{ω}$
2		frsucmpt2.2	$⊢ y = x \to E = C$
3		frsucmpt2.3	$⊢ y = F (B) \to E = D$
4		nfcv	$⊢ \underline{Ⅎ} y A$
5		nfcv	$⊢ \underline{Ⅎ} y B$
6		nfcv	$⊢ \underline{Ⅎ} y D$
7	2	cbvmptv	$⊢ (y \in V ⟼ E) = (x \in V ⟼ C)$
8		rdgeq1	$⊢ (y \in V ⟼ E) = (x \in V ⟼ C) \to rec ((y \in V ⟼ E), A) = rec ((x \in V ⟼ C), A)$
9	7 8	ax-mp	$⊢ rec ((y \in V ⟼ E), A) = rec ((x \in V ⟼ C), A)$
10	9	reseq1i	$⊢ {rec ((y \in V ⟼ E), A) ↾}_{ω} = {rec ((x \in V ⟼ C), A) ↾}_{ω}$
11	1 10	eqtr4i	$⊢ F = {rec ((y \in V ⟼ E), A) ↾}_{ω}$
12	4 5 6 11 3	frsucmpt	$⊢ (B \in ω \land D \in V) \to F (suc B) = D$

Metamath Proof Explorer

Theorem frsucmpt2

Proof