wfr2

Description: The Principle of Well-Ordered Recursion, part 2 of 3. Next, we show that the value of F at any X e. A is G applied to all "previous" values of F . (Contributed by Scott Fenton, 18-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Hypothesis	wfr2.1	$⊢ F = wrecs (R, A, G)$
	Assertion	wfr2	$⊢ ((R We A \land R Se A) \land X \in A) \to F (X) = G ({F ↾}_{Pred (R, A, X)})$

Proof

Step	Hyp	Ref	Expression
1		wfr2.1	$⊢ F = wrecs (R, A, G)$
2	1	wfr1	$⊢ (R We A \land R Se A) \to F Fn A$
3	2	fndmd	$⊢ (R We A \land R Se A) \to dom F = A$
4	3	eleq2d	$⊢ (R We A \land R Se A) \to (X \in dom F \leftrightarrow X \in A)$
5	4	biimpar	$⊢ ((R We A \land R Se A) \land X \in A) \to X \in dom F$
6	1	wfr2a	$⊢ ((R We A \land R Se A) \land X \in dom F) \to F (X) = G ({F ↾}_{Pred (R, A, X)})$
7	5 6	syldan	$⊢ ((R We A \land R Se A) \land X \in A) \to F (X) = G ({F ↾}_{Pred (R, A, X)})$

Metamath Proof Explorer

Theorem wfr2

Proof