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

Theorem tfinds 4832
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 4820 . . . . 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 4584 . . . . . . 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 2749 . . . . . . . . 9  |-  F/ y A. y  e.  x  ch
14 nfv 1629 . . . . . . . . 9  |-  F/ y
ph
1513, 14nfim 1832 . . . . . . . 8  |-  F/ y ( A. y  e.  x  ch  ->  ph )
16 vex 2952 . . . . . . . . . . . . 13  |-  y  e. 
_V
1716sucid 4653 . . . . . . . . . . . 12  |-  y  e. 
suc  y
181rspcv 3041 . . . . . . . . . . . 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 2897 . . . . . . . . . . . 12  |-  ( x  =  suc  y  -> 
( A. z  e.  x  [ z  /  x ] ph  <->  A. z  e.  suc  y [ z  /  x ] ph ) )
23 nfv 1629 . . . . . . . . . . . . . . 15  |-  F/ x ch
2423, 1sbie 2124 . . . . . . . . . . . . . 14  |-  ( [ y  /  x ] ph 
<->  ch )
25 sbequ 2140 . . . . . . . . . . . . . 14  |-  ( y  =  z  ->  ( [ y  /  x ] ph  <->  [ z  /  x ] ph ) )
2624, 25syl5bbr 251 . . . . . . . . . . . . 13  |-  ( y  =  z  ->  ( ch 
<->  [ z  /  x ] ph ) )
2726cbvralv 2925 . . . . . . . . . . . 12  |-  ( A. y  e.  x  ch  <->  A. z  e.  x  [
z  /  x ] ph )
28 cbvralsv 2936 . . . . . . . . . . . 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 2816 . . . . . . 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 4830 1  |-  ( A  e.  On  ->  ta )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    = wceq 1652   [wsb 1658    e. wcel 1725   A.wral 2698   E.wrex 2699   (/)c0 3621   Ord word 4573   Oncon0 4574   Lim wlim 4575   suc csuc 4576
This theorem is referenced by:  tfindsg  4833  tfindes  4835  tfinds3  4837  oa0r  6775  om0r  6776  om1r  6779  oe1m  6781  oeoalem  6832  r1sdom  7693  r1tr  7695  alephon  7943  alephcard  7944  alephordi  7948  rdgprc  25415
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4323  ax-nul 4331  ax-pr 4396  ax-un 4694
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2703  df-rex 2704  df-rab 2707  df-v 2951  df-sbc 3155  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-pss 3329  df-nul 3622  df-if 3733  df-pw 3794  df-sn 3813  df-pr 3814  df-tp 3815  df-op 3816  df-uni 4009  df-br 4206  df-opab 4260  df-tr 4296  df-eprel 4487  df-po 4496  df-so 4497  df-fr 4534  df-we 4536  df-ord 4577  df-on 4578  df-lim 4579  df-suc 4580
  Copyright terms: Public domain W3C validator