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

Theorem tfinds 4772
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. Theorem Schema 4 of [Suppes] p. 197. (Contributed by NM, 16-Apr-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Hypotheses
Ref Expression
tfinds.1  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
tfinds.2  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
tfinds.3  |-  ( x  =  suc  y  -> 
( ph  <->  th ) )
tfinds.4  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
tfinds.5  |-  ps
tfinds.6  |-  ( y  e.  On  ->  ( ch  ->  th ) )
tfinds.7  |-  ( Lim  x  ->  ( A. y  e.  x  ch  ->  ph ) )
Assertion
Ref Expression
tfinds  |-  ( A  e.  On  ->  ta )
Distinct variable groups:    x, y    x, A    ch, x    ta, x    ph, y
Allowed substitution hints:    ph( x)    ps( x, y)    ch( y)    th( x, y)    ta( y)    A( y)

Proof of Theorem tfinds
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 tfinds.2 . 2  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
2 tfinds.4 . 2  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
3 dflim3 4760 . . . . 5  |-  ( Lim  x  <->  ( Ord  x  /\  -.  ( x  =  (/)  \/  E. y  e.  On  x  =  suc  y ) ) )
43notbii 288 . . . 4  |-  ( -. 
Lim  x  <->  -.  ( Ord  x  /\  -.  (
x  =  (/)  \/  E. y  e.  On  x  =  suc  y ) ) )
5 iman 414 . . . . 5  |-  ( ( Ord  x  ->  (
x  =  (/)  \/  E. y  e.  On  x  =  suc  y ) )  <->  -.  ( Ord  x  /\  -.  ( x  =  (/)  \/ 
E. y  e.  On  x  =  suc  y ) ) )
6 eloni 4525 . . . . . . 7  |-  ( x  e.  On  ->  Ord  x )
7 pm2.27 37 . . . . . . 7  |-  ( Ord  x  ->  ( ( Ord  x  ->  ( x  =  (/)  \/  E. y  e.  On  x  =  suc  y ) )  -> 
( x  =  (/)  \/ 
E. y  e.  On  x  =  suc  y ) ) )
86, 7syl 16 . . . . . 6  |-  ( x  e.  On  ->  (
( Ord  x  ->  ( x  =  (/)  \/  E. y  e.  On  x  =  suc  y ) )  ->  ( x  =  (/)  \/  E. y  e.  On  x  =  suc  y ) ) )
9 tfinds.5 . . . . . . . . 9  |-  ps
10 tfinds.1 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
119, 10mpbiri 225 . . . . . . . 8  |-  ( x  =  (/)  ->  ph )
1211a1d 23 . . . . . . 7  |-  ( x  =  (/)  ->  ( A. y  e.  x  ch  ->  ph ) )
13 nfra1 2692 . . . . . . . . 9  |-  F/ y A. y  e.  x  ch
14 nfv 1626 . . . . . . . . 9  |-  F/ y
ph
1513, 14nfim 1822 . . . . . . . 8  |-  F/ y ( A. y  e.  x  ch  ->  ph )
16 vex 2895 . . . . . . . . . . . . 13  |-  y  e. 
_V
1716sucid 4594 . . . . . . . . . . . 12  |-  y  e. 
suc  y
181rspcv 2984 . . . . . . . . . . . 12  |-  ( y  e.  suc  y  -> 
( A. x  e. 
suc  y ph  ->  ch ) )
1917, 18ax-mp 8 . . . . . . . . . . 11  |-  ( A. x  e.  suc  y ph  ->  ch )
20 tfinds.6 . . . . . . . . . . 11  |-  ( y  e.  On  ->  ( ch  ->  th ) )
2119, 20syl5 30 . . . . . . . . . 10  |-  ( y  e.  On  ->  ( A. x  e.  suc  y ph  ->  th )
)
22 raleq 2840 . . . . . . . . . . . 12  |-  ( x  =  suc  y  -> 
( A. z  e.  x  [ z  /  x ] ph  <->  A. z  e.  suc  y [ z  /  x ] ph ) )
23 nfv 1626 . . . . . . . . . . . . . . 15  |-  F/ x ch
2423, 1sbie 2064 . . . . . . . . . . . . . 14  |-  ( [ y  /  x ] ph 
<->  ch )
25 sbequ 2086 . . . . . . . . . . . . . 14  |-  ( y  =  z  ->  ( [ y  /  x ] ph  <->  [ z  /  x ] ph ) )
2624, 25syl5bbr 251 . . . . . . . . . . . . 13  |-  ( y  =  z  ->  ( ch 
<->  [ z  /  x ] ph ) )
2726cbvralv 2868 . . . . . . . . . . . 12  |-  ( A. y  e.  x  ch  <->  A. z  e.  x  [
z  /  x ] ph )
28 cbvralsv 2879 . . . . . . . . . . . 12  |-  ( A. x  e.  suc  y ph  <->  A. z  e.  suc  y [ z  /  x ] ph )
2922, 27, 283bitr4g 280 . . . . . . . . . . 11  |-  ( x  =  suc  y  -> 
( A. y  e.  x  ch  <->  A. x  e.  suc  y ph )
)
3029imbi1d 309 . . . . . . . . . 10  |-  ( x  =  suc  y  -> 
( ( A. y  e.  x  ch  ->  th )  <->  ( A. x  e.  suc  y ph  ->  th ) ) )
3121, 30syl5ibrcom 214 . . . . . . . . 9  |-  ( y  e.  On  ->  (
x  =  suc  y  ->  ( A. y  e.  x  ch  ->  th )
) )
32 tfinds.3 . . . . . . . . . . 11  |-  ( x  =  suc  y  -> 
( ph  <->  th ) )
3332biimprd 215 . . . . . . . . . 10  |-  ( x  =  suc  y  -> 
( th  ->  ph )
)
3433a1i 11 . . . . . . . . 9  |-  ( y  e.  On  ->  (
x  =  suc  y  ->  ( th  ->  ph )
) )
3531, 34syldd 63 . . . . . . . 8  |-  ( y  e.  On  ->  (
x  =  suc  y  ->  ( A. y  e.  x  ch  ->  ph )
) )
3615, 35rexlimi 2759 . . . . . . 7  |-  ( E. y  e.  On  x  =  suc  y  ->  ( A. y  e.  x  ch  ->  ph ) )
3712, 36jaoi 369 . . . . . 6  |-  ( ( x  =  (/)  \/  E. y  e.  On  x  =  suc  y )  -> 
( A. y  e.  x  ch  ->  ph )
)
388, 37syl6 31 . . . . 5  |-  ( x  e.  On  ->  (
( Ord  x  ->  ( x  =  (/)  \/  E. y  e.  On  x  =  suc  y ) )  ->  ( A. y  e.  x  ch  ->  ph ) ) )
395, 38syl5bir 210 . . . 4  |-  ( x  e.  On  ->  ( -.  ( Ord  x  /\  -.  ( x  =  (/)  \/ 
E. y  e.  On  x  =  suc  y ) )  ->  ( A. y  e.  x  ch  ->  ph ) ) )
404, 39syl5bi 209 . . 3  |-  ( x  e.  On  ->  ( -.  Lim  x  ->  ( A. y  e.  x  ch  ->  ph ) ) )
41 tfinds.7 . . 3  |-  ( Lim  x  ->  ( A. y  e.  x  ch  ->  ph ) )
4240, 41pm2.61d2 154 . 2  |-  ( x  e.  On  ->  ( A. y  e.  x  ch  ->  ph ) )
431, 2, 42tfis3 4770 1  |-  ( A  e.  On  ->  ta )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    = wceq 1649   [wsb 1655    e. wcel 1717   A.wral 2642   E.wrex 2643   (/)c0 3564   Ord word 4514   Oncon0 4515   Lim wlim 4516   suc csuc 4517
This theorem is referenced by:  tfindsg  4773  tfindes  4775  tfinds3  4777  oa0r  6711  om0r  6712  om1r  6715  oe1m  6717  oeoalem  6768  r1sdom  7626  r1tr  7628  alephon  7876  alephcard  7877  alephordi  7881  rdgprc  25168
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 2361  ax-sep 4264  ax-nul 4272  ax-pr 4337  ax-un 4634
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 2235  df-mo 2236  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-ral 2647  df-rex 2648  df-rab 2651  df-v 2894  df-sbc 3098  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-pss 3272  df-nul 3565  df-if 3676  df-pw 3737  df-sn 3756  df-pr 3757  df-tp 3758  df-op 3759  df-uni 3951  df-br 4147  df-opab 4201  df-tr 4237  df-eprel 4428  df-po 4437  df-so 4438  df-fr 4475  df-we 4477  df-ord 4518  df-on 4519  df-lim 4520  df-suc 4521
  Copyright terms: Public domain W3C validator