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	$⊢ F = recs (G)$
	Assertion	tfr1	$⊢ F Fn On$

Proof

Step	Hyp	Ref	Expression
1		tfr.1	$⊢ F = recs (G)$
2		eqid	$⊢ \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = G ({f ↾}_{y}))\} = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = G ({f ↾}_{y}))\}$
3	2	tfrlem7	$⊢ Fun recs (G)$
4	2	tfrlem14	$⊢ dom recs (G) = On$
5		df-fn	$⊢ recs (G) Fn On \leftrightarrow (Fun recs (G) \land dom recs (G) = On)$
6	3 4 5	mpbir2an	$⊢ recs (G) Fn On$
7	1	fneq1i	$⊢ F Fn On \leftrightarrow recs (G) Fn On$
8	6 7	mpbir	$⊢ F Fn On$

Metamath Proof Explorer

Theorem tfr1

Proof