wfr1

Description: The Principle of Well-Ordered Recursion, part 1 of 3. We start with an arbitrary function G . Then, using a base class A and a set-like well-ordering R of A , we define a function F . This function is said to be defined by "well-ordered recursion". The purpose of these three theorems is to demonstrate the properties of F . We begin by showing that F is a function over A . (Contributed by Scott Fenton, 22-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by Scott Fenton, 18-Nov-2024)

		Ref	Expression
	Hypothesis	wfr1.1	$⊢ F = wrecs (R, A, G)$
	Assertion	wfr1	$⊢ (R We A \land R Se A) \to F Fn A$

Proof

Step	Hyp	Ref	Expression
1		wfr1.1	$⊢ F = wrecs (R, A, G)$
2		wefr	$⊢ R We A \to R Fr A$
3	2	adantr	$⊢ (R We A \land R Se A) \to R Fr A$
4		weso	$⊢ R We A \to R Or A$
5		sopo	$⊢ R Or A \to R Po A$
6	4 5	syl	$⊢ R We A \to R Po A$
7	6	adantr	$⊢ (R We A \land R Se A) \to R Po A$
8		simpr	$⊢ (R We A \land R Se A) \to R Se A$
9		df-wrecs	$⊢ wrecs (R, A, G) = frecs (R, A, G \circ 2^{nd})$
10	1 9	eqtri	$⊢ F = frecs (R, A, G \circ 2^{nd})$
11	10	fpr1	$⊢ (R Fr A \land R Po A \land R Se A) \to F Fn A$
12	3 7 8 11	syl3anc	$⊢ (R We A \land R Se A) \to F Fn A$

Metamath Proof Explorer

Theorem wfr1

Proof