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

Theorem tfinds3 4786
Description: Principle of Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction hypothesis for successors, and the induction hypothesis for limit ordinals. (Contributed by NM, 6-Jan-2005.) (Revised by David Abernethy, 21-Jun-2011.)
Hypotheses
Ref Expression
tfinds3.1  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
tfinds3.2  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
tfinds3.3  |-  ( x  =  suc  y  -> 
( ph  <->  th ) )
tfinds3.4  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
tfinds3.5  |-  ( et 
->  ps )
tfinds3.6  |-  ( y  e.  On  ->  ( et  ->  ( ch  ->  th ) ) )
tfinds3.7  |-  ( Lim  x  ->  ( et  ->  ( A. y  e.  x  ch  ->  ph )
) )
Assertion
Ref Expression
tfinds3  |-  ( A  e.  On  ->  ( et  ->  ta ) )
Distinct variable groups:    x, A    ph, y    ch, x    ta, x    x, y, et
Allowed substitution hints:    ph( x)    ps( x, y)    ch( y)    th( x, y)    ta( y)    A( y)

Proof of Theorem tfinds3
StepHypRef Expression
1 tfinds3.1 . . 3  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
21imbi2d 308 . 2  |-  ( x  =  (/)  ->  ( ( et  ->  ph )  <->  ( et  ->  ps ) ) )
3 tfinds3.2 . . 3  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
43imbi2d 308 . 2  |-  ( x  =  y  ->  (
( et  ->  ph )  <->  ( et  ->  ch )
) )
5 tfinds3.3 . . 3  |-  ( x  =  suc  y  -> 
( ph  <->  th ) )
65imbi2d 308 . 2  |-  ( x  =  suc  y  -> 
( ( et  ->  ph )  <->  ( et  ->  th ) ) )
7 tfinds3.4 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
87imbi2d 308 . 2  |-  ( x  =  A  ->  (
( et  ->  ph )  <->  ( et  ->  ta )
) )
9 tfinds3.5 . 2  |-  ( et 
->  ps )
10 tfinds3.6 . . 3  |-  ( y  e.  On  ->  ( et  ->  ( ch  ->  th ) ) )
1110a2d 24 . 2  |-  ( y  e.  On  ->  (
( et  ->  ch )  ->  ( et  ->  th ) ) )
12 r19.21v 2738 . . 3  |-  ( A. y  e.  x  ( et  ->  ch )  <->  ( et  ->  A. y  e.  x  ch ) )
13 tfinds3.7 . . . 4  |-  ( Lim  x  ->  ( et  ->  ( A. y  e.  x  ch  ->  ph )
) )
1413a2d 24 . . 3  |-  ( Lim  x  ->  ( ( et  ->  A. y  e.  x  ch )  ->  ( et 
->  ph ) ) )
1512, 14syl5bi 209 . 2  |-  ( Lim  x  ->  ( A. y  e.  x  ( et  ->  ch )  -> 
( et  ->  ph )
) )
162, 4, 6, 8, 9, 11, 15tfinds 4781 1  |-  ( A  e.  On  ->  ( et  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1717   A.wral 2651   (/)c0 3573   Oncon0 4524   Lim wlim 4525   suc csuc 4526
This theorem is referenced by:  oacl  6717  omcl  6718  oecl  6719  oawordri  6731  oaass  6742  oarec  6743  omordi  6747  omwordri  6753  odi  6760  omass  6761  oen0  6767  oewordri  6773  oeworde  6774  oeoelem  6779  omabs  6828
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pr 4346  ax-un 4643
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-rab 2660  df-v 2903  df-sbc 3107  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-pss 3281  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-tp 3767  df-op 3768  df-uni 3960  df-br 4156  df-opab 4210  df-tr 4246  df-eprel 4437  df-po 4446  df-so 4447  df-fr 4484  df-we 4486  df-ord 4527  df-on 4528  df-lim 4529  df-suc 4530
  Copyright terms: Public domain W3C validator