Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  tfrlem16 Structured version   Unicode version

Theorem tfrlem16 7115
 Description: Lemma for finite recursion. Without assuming ax-rep 4533, we can show that the domain of the constructed function is a limit ordinal, and hence contains all the finite ordinals. (Contributed by Mario Carneiro, 14-Nov-2014.)
Hypothesis
Ref Expression
tfrlem.1
Assertion
Ref Expression
tfrlem16 recs
Distinct variable group:   ,,,
Allowed substitution hints:   (,,)

Proof of Theorem tfrlem16
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 tfrlem.1 . . . 4
21tfrlem8 7106 . . 3 recs
3 ordzsl 6682 . . 3 recs recs recs recs
42, 3mpbi 211 . 2 recs recs recs
5 res0 5124 . . . . . . 7 recs
6 0ex 4552 . . . . . . 7
75, 6eqeltri 2506 . . . . . 6 recs
8 0elon 5491 . . . . . . 7
91tfrlem15 7114 . . . . . . 7 recs recs
108, 9ax-mp 5 . . . . . 6 recs recs
117, 10mpbir 212 . . . . 5 recs
12 n0i 3766 . . . . 5 recs recs
1311, 12ax-mp 5 . . . 4 recs
1413pm2.21i 134 . . 3 recs recs
151tfrlem13 7112 . . . . 5 recs
16 simpr 462 . . . . . . . . . 10 recs recs
17 df-suc 5444 . . . . . . . . . 10
1816, 17syl6eq 2479 . . . . . . . . 9 recs recs
1918reseq2d 5120 . . . . . . . 8 recs recs recs recs
201tfrlem6 7104 . . . . . . . . 9 recs
21 resdm 5161 . . . . . . . . 9 recs recs recs recs
2220, 21ax-mp 5 . . . . . . . 8 recs recs recs
23 resundi 5133 . . . . . . . 8 recs recs recs
2419, 22, 233eqtr3g 2486 . . . . . . 7 recs recs recs recs
25 vex 3084 . . . . . . . . . . 11
2625sucid 5517 . . . . . . . . . 10
2726, 16syl5eleqr 2517 . . . . . . . . 9 recs recs
281tfrlem9a 7108 . . . . . . . . 9 recs recs
2927, 28syl 17 . . . . . . . 8 recs recs
30 snex 4658 . . . . . . . . 9 recs
311tfrlem7 7105 . . . . . . . . . 10 recs
32 funressn 6088 . . . . . . . . . 10 recs recs recs
3331, 32ax-mp 5 . . . . . . . . 9 recs recs
3430, 33ssexi 4565 . . . . . . . 8 recs
35 unexg 6602 . . . . . . . 8 recs recs recs recs
3629, 34, 35sylancl 666 . . . . . . 7 recs recs recs
3724, 36eqeltrd 2510 . . . . . 6 recs recs
3837rexlimiva 2913 . . . . 5 recs recs
3915, 38mto 179 . . . 4 recs
4039pm2.21i 134 . . 3 recs recs
41 id 23 . . 3 recs recs
4214, 40, 413jaoi 1327 . 2 recs recs recs recs
434, 42ax-mp 5 1 recs
 Colors of variables: wff setvar class Syntax hints:   wn 3   wb 187   wa 370   w3o 981   wceq 1437   wcel 1868  cab 2407  wral 2775  wrex 2776  cvv 3081   cun 3434   wss 3436  c0 3761  csn 3996  cop 4002   cdm 4849   cres 4851   wrel 4854   word 5437  con0 5438   wlim 5439   csuc 5440   wfun 5591   wfn 5592  cfv 5597  recscrecs 7093 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-wrecs 7032  df-recs 7094 This theorem is referenced by:  tfr1a  7116
 Copyright terms: Public domain W3C validator