Metamath Proof Explorer

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 ${⊢}{F}=\mathrm{recs}\left({G}\right)$
Assertion tfr1 ${⊢}{F}Fn\mathrm{On}$

Proof

Step Hyp Ref Expression
1 tfr.1 ${⊢}{F}=\mathrm{recs}\left({G}\right)$
2 eqid ${⊢}\left\{{f}|\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({f}Fn{x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)={G}\left({{f}↾}_{{y}}\right)\right)\right\}=\left\{{f}|\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({f}Fn{x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)={G}\left({{f}↾}_{{y}}\right)\right)\right\}$
3 2 tfrlem7 ${⊢}\mathrm{Fun}\mathrm{recs}\left({G}\right)$
4 2 tfrlem14 ${⊢}\mathrm{dom}\mathrm{recs}\left({G}\right)=\mathrm{On}$
5 df-fn ${⊢}\mathrm{recs}\left({G}\right)Fn\mathrm{On}↔\left(\mathrm{Fun}\mathrm{recs}\left({G}\right)\wedge \mathrm{dom}\mathrm{recs}\left({G}\right)=\mathrm{On}\right)$
6 3 4 5 mpbir2an ${⊢}\mathrm{recs}\left({G}\right)Fn\mathrm{On}$
7 1 fneq1i ${⊢}{F}Fn\mathrm{On}↔\mathrm{recs}\left({G}\right)Fn\mathrm{On}$
8 6 7 mpbir ${⊢}{F}Fn\mathrm{On}$