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 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)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | wfr1.1 | ⊢ 𝑅 We 𝐴 | |
| wfr1.2 | ⊢ 𝑅 Se 𝐴 | ||
| wfr1.3 | ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 ) | ||
| Assertion | wfr1 | ⊢ 𝐹 Fn 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wfr1.1 | ⊢ 𝑅 We 𝐴 | |
| 2 | wfr1.2 | ⊢ 𝑅 Se 𝐴 | |
| 3 | wfr1.3 | ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 ) | |
| 4 | 1 2 3 | wfrfun | ⊢ Fun 𝐹 |
| 5 | eqid | ⊢ ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) = ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) | |
| 6 | 1 2 3 5 | wfrlem16 | ⊢ dom 𝐹 = 𝐴 |
| 7 | df-fn | ⊢ ( 𝐹 Fn 𝐴 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) ) | |
| 8 | 4 6 7 | mpbir2an | ⊢ 𝐹 Fn 𝐴 |