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 | ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 ) | |
| Assertion | wfr1 | ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 Fn 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wfr1.1 | ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 ) | |
| 2 | wefr | ⊢ ( 𝑅 We 𝐴 → 𝑅 Fr 𝐴 ) | |
| 3 | 2 | adantr | ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝑅 Fr 𝐴 ) |
| 4 | weso | ⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 ) | |
| 5 | sopo | ⊢ ( 𝑅 Or 𝐴 → 𝑅 Po 𝐴 ) | |
| 6 | 4 5 | syl | ⊢ ( 𝑅 We 𝐴 → 𝑅 Po 𝐴 ) |
| 7 | 6 | adantr | ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝑅 Po 𝐴 ) |
| 8 | simpr | ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝑅 Se 𝐴 ) | |
| 9 | df-wrecs | ⊢ wrecs ( 𝑅 , 𝐴 , 𝐺 ) = frecs ( 𝑅 , 𝐴 , ( 𝐺 ∘ 2nd ) ) | |
| 10 | 1 9 | eqtri | ⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , ( 𝐺 ∘ 2nd ) ) |
| 11 | 10 | fpr1 | ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 Fn 𝐴 ) |
| 12 | 3 7 8 11 | syl3anc | ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 Fn 𝐴 ) |