Theorem tfr1 8370

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

Hypothesis

Ref	Expression
tfr.1	⊢ 𝐹 = recs(𝐺)

Assertion

Ref	Expression
tfr1	⊢ 𝐹 Fn On

Proof of Theorem tfr1

Dummy variables 𝑥 𝑓 𝑦 are mutually distinct and distinct from all other variables.

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

Syntax hints:   ∧ wa 399   = wceq 1562  {cab 2742  ∀wral 3078  ∃wrex 3088  dom cdm 5649   ↾ cres 5651  Oncon0 6348  Fun wfun 6517   Fn wfn 6518  ‘cfv 6523  recscrecs 8343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-rep 5229  ax-sep 5248  ax-nul 5258  ax-pr 5392  ax-un 7720

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3079  df-rex 3089  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-pred 6290  df-ord 6351  df-on 6352  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-ov 7401  df-2nd 7973  df-frecs 8264  df-wrecs 8295  df-recs 8344

This theorem is referenced by:  tfr2  8371  tfr3  8372  recsfnon  8376  rdgfnon  8391  dfac8alem  9987  dfac12lem1  10102  dfac12lem2  10103  zorn2lem1  10455  zorn2lem2  10456  zorn2lem4  10458  zorn2lem5  10459  zorn2lem6  10460  zorn2lem7  10461  ttukeylem3  10470  ttukeylem5  10472  ttukeylem6  10473  madeval  27927  newval  27930  madef  27931  onvf1odlem3  35452  onvf1odlem4  35453  onvf1od  35454  dnnumch1  43626  dnnumch3lem  43628  dnnumch3  43629  aomclem6  43641