Theorem tfr1

Description: Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of TakeutiZaring p. 47. We start with an arbitrary class G , normally a function, and define a class A of all "acceptable" functions. The final function we're interested in is the union F = recs ( G ) of them. F is then said to be defined by transfinite recursion. The purpose of the 3 parts of this theorem is to demonstrate properties of F . In this first part we show that F is a function whose domain is all ordinal numbers. (Contributed by NM, 17-Aug-1994) (Revised by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Hypothesis	tfr.1	⊢ 𝐹 = recs ( 𝐺 )
Assertion	tfr1	⊢ 𝐹 Fn On

Proof

Step	Hyp	Ref	Expression
1		tfr.1	⊢ 𝐹 = recs ( 𝐺 )
2		eqid	⊢ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ 𝑦 ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
3	2	tfrlem7	⊢ Fun recs ( 𝐺 )
4	2	tfrlem14	⊢ dom recs ( 𝐺 ) = On
5		df-fn	⊢ ( recs ( 𝐺 ) Fn On ↔ ( Fun recs ( 𝐺 ) ∧ dom recs ( 𝐺 ) = On ) )
6	3 4 5	mpbir2an	⊢ recs ( 𝐺 ) Fn On
7	1	fneq1i	⊢ ( 𝐹 Fn On ↔ recs ( 𝐺 ) Fn On )
8	6 7	mpbir	⊢ 𝐹 Fn On