Theorem tfr1 5336

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 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.

Hypotheses

Ref	Expression
tfr.1	|- A = {f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}
tfr.2	|- F = U.A

Assertion

Ref	Expression
tfr1	|- F Fn On

Distinct variable groups:   x,f,A   x,y,F,f   x,G,y,f

Proof of Theorem tfr1

Step	Hyp	Ref	Expression
1		df-fn 4174	. 2 |- (F Fn On <-> (Fun F /\ dom F = On))
2		tfr.1	. . 3 |- A = {f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}
3		tfr.2	. . 3 |- F = U.A
4	2, 3	tfrlem7 5329	. 2 |- Fun F
5		eqid 2170	. . 3 |- (F u. {<.dom F, (G` (F |` dom F))>.}) = (F u. {<.dom F, (G` (F |` dom F))>.})
6	2, 3, 5	tfrlem13 5335	. 2 |- dom F = On
7	1, 4, 6	mpbir2an 1062	1 |- F Fn On

Syntax hints:   /\ wa 433   = wceq 1615  {cab 2157  A.wral 2385  E.wrex 2386   u. cun 2857  {csn 3270  <.cop 3272  U.cuni 3398  Oncon0 3843  dom cdm 4151   |` cres 4153  Fun wfun 4157   Fn wfn 4158  ` cfv 4163

This theorem is referenced by:  tfr3 5338  rdgfnon 5351  ordtypelem2 5960  ordtypelem4 5962  ordtypelem5 5963  ordtypelem6 5964  ordtypelem7 5965  aceq8alem 6263  cfsmolem 6352  numthlem 6429  zorn2lem2 6436  zorn2lem4 6438  zorn2lem6 6440  ordtypelem2OLD 16461  ordtypelem4OLD 16463  ordtypelem5OLD 16464  ordtypelem6OLD 16465  ordtypelem7OLD 16466

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-rab 2392  df-v 2571  df-sbc 2731  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-iun 3470  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-id 3779  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-suc 3849  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-fv 4179

Copyright terms: Public domain