Metamath Proof Explorer


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 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 R We A
wfr1.2 R Se A
wfr1.3 F = wrecs R A G
Assertion wfr1 F Fn A

Proof

Step Hyp Ref Expression
1 wfr1.1 R We A
2 wfr1.2 R Se A
3 wfr1.3 F = wrecs R A G
4 1 2 3 wfrfun Fun F
5 eqid F z G F Pred R A z = F z G F Pred R A z
6 1 2 3 5 wfrlem16 dom F = A
7 df-fn F Fn A Fun F dom F = A
8 4 6 7 mpbir2an F Fn A