Theorem 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 /\ R Se A ) -> F Fn A )

Proof

Step	Hyp	Ref	Expression
1		wfr1.1	|- F = wrecs ( R , A , G )
2		wefr	|- ( R We A -> R Fr A )
3	2	adantr	|- ( ( R We A /\ R Se A ) -> R Fr A )
4		weso	|- ( R We A -> R Or A )
5		sopo	|- ( R Or A -> R Po A )
6	4 5	syl	|- ( R We A -> R Po A )
7	6	adantr	|- ( ( R We A /\ R Se A ) -> R Po A )
8		simpr	|- ( ( R We A /\ R Se A ) -> R Se A )
9		df-wrecs	|- wrecs ( R , A , G ) = frecs ( R , A , ( G o. 2nd ) )
10	1 9	eqtri	|- F = frecs ( R , A , ( G o. 2nd ) )
11	10	fpr1	|- ( ( R Fr A /\ R Po A /\ R Se A ) -> F Fn A )
12	3 7 8 11	syl3anc	|- ( ( R We A /\ R Se A ) -> F Fn A )