Theorem wfr1

Description: The Principle of Well-Founded 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-founded 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 𝐴

Proof

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 𝐴