ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  tfri1 Structured version   GIF version

Theorem tfri1 5838
Description: Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of [TakeutiZaring] p. 47, with an additional condition.

The condition is that 𝐺 is defined "everywhere" and here is stated as (𝐺x) V. Alternatively x Onf(f Fn xf dom 𝐺) would suffice.

Given a function 𝐺 satisfying that condition, we define a class A 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 Jim Kingdon, 4-May-2019.) (Revised by Mario Carneiro, 24-May-2019.)

Hypotheses
Ref Expression
tfri1.1 𝐹 = recs(𝐺)
tfri1.2 (Fun 𝐺 (𝐺x) V)
Assertion
Ref Expression
tfri1 𝐹 Fn On
Distinct variable group:   x,𝐺
Allowed substitution hint:   𝐹(x)

Proof of Theorem tfri1
Dummy variables f g u w y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2022 . . . 4 {wy On (w Fn y z y (wz) = (𝐺‘(wz)))} = {wy On (w Fn y z y (wz) = (𝐺‘(wz)))}
21tfrlem7 5820 . . 3 Fun recs(𝐺)
3 eqid 2022 . . . . 5 {gz On (g Fn z u z (gu) = (𝐺‘(gu)))} = {gz On (g Fn z u z (gu) = (𝐺‘(gu)))}
43tfrlem3 5813 . . . 4 {gz On (g Fn z u z (gu) = (𝐺‘(gu)))} = {fx On (f Fn x y x (fy) = (𝐺‘(fy)))}
5 tfri1.2 . . . 4 (Fun 𝐺 (𝐺x) V)
64, 5tfrlemi14 5834 . . 3 dom recs(𝐺) = On
7 df-fn 4799 . . 3 (recs(𝐺) Fn On ↔ (Fun recs(𝐺) dom recs(𝐺) = On))
82, 6, 7mpbir2an 837 . 2 recs(𝐺) Fn On
9 tfri1.1 . . 3 𝐹 = recs(𝐺)
109fneq1i 4886 . 2 (𝐹 Fn On ↔ recs(𝐺) Fn On)
118, 10mpbir 134 1 𝐹 Fn On
Colors of variables: wff set class
Syntax hints:   wa 97   = wceq 1373   wcel 1375  {cab 2008  wral 2282  wrex 2283  Vcvv 2533  Oncon0 4024  dom cdm 4238  cres 4240  Fun wfun 4790   Fn wfn 4791  cfv 4796  recscrecs 5806
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1315  ax-7 1316  ax-gen 1317  ax-ie1 1362  ax-ie2 1363  ax-8 1377  ax-10 1378  ax-11 1379  ax-i12 1380  ax-bnd 1381  ax-4 1382  ax-13 1386  ax-14 1387  ax-17 1401  ax-i9 1405  ax-ial 1410  ax-i5r 1411  ax-ext 2004  ax-coll 3824  ax-sep 3827  ax-pow 3879  ax-pr 3896  ax-un 4093  ax-setind 4174
This theorem depends on definitions:  df-bi 110  df-3an 877  df-tru 1231  df-fal 1232  df-nf 1329  df-sb 1628  df-eu 1884  df-mo 1885  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ne 2188  df-ral 2287  df-rex 2288  df-reu 2289  df-rab 2291  df-v 2535  df-sbc 2740  df-csb 2829  df-dif 2898  df-un 2900  df-in 2902  df-ss 2909  df-nul 3203  df-pw 3313  df-sn 3333  df-pr 3334  df-op 3336  df-uni 3533  df-iun 3611  df-br 3717  df-opab 3771  df-mpt 3772  df-tr 3807  df-id 3983  df-iord 4027  df-on 4028  df-suc 4031  df-xp 4244  df-rel 4245  df-cnv 4246  df-co 4247  df-dm 4248  df-rn 4249  df-res 4250  df-ima 4251  df-iota 4761  df-fun 4798  df-fn 4799  df-f 4800  df-f1 4801  df-fo 4802  df-f1o 4803  df-fv 4804  df-recs 5807
This theorem is referenced by:  tfri2  5839  tfri3  5840
  Copyright terms: Public domain W3C validator