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

Theorem tfinds2 6671
Description: Transfinite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last three are the basis and the induction hypotheses (for successor and limit ordinals respectively). Theorem Schema 4 of [Suppes] p. 197. The wff  ta is an auxiliary antecedent to help shorten proofs using this theorem. (Contributed by NM, 4-Sep-2004.)
Hypotheses
Ref Expression
tfinds2.1  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
tfinds2.2  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
tfinds2.3  |-  ( x  =  suc  y  -> 
( ph  <->  th ) )
tfinds2.4  |-  ( ta 
->  ps )
tfinds2.5  |-  ( y  e.  On  ->  ( ta  ->  ( ch  ->  th ) ) )
tfinds2.6  |-  ( Lim  x  ->  ( ta  ->  ( A. y  e.  x  ch  ->  ph )
) )
Assertion
Ref Expression
tfinds2  |-  ( x  e.  On  ->  ( ta  ->  ph ) )
Distinct variable groups:    x, y, ta    ps, x    ch, x    th, x    ph, y
Allowed substitution hints:    ph( x)    ps( y)    ch( y)    th( y)

Proof of Theorem tfinds2
StepHypRef Expression
1 tfinds2.4 . . 3  |-  ( ta 
->  ps )
2 0ex 4572 . . . 4  |-  (/)  e.  _V
3 tfinds2.1 . . . . 5  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
43imbi2d 316 . . . 4  |-  ( x  =  (/)  ->  ( ( ta  ->  ph )  <->  ( ta  ->  ps ) ) )
52, 4sbcie 3361 . . 3  |-  ( [. (/)  /  x ]. ( ta 
->  ph )  <->  ( ta  ->  ps ) )
61, 5mpbir 209 . 2  |-  [. (/)  /  x ]. ( ta  ->  ph )
7 vex 3111 . . . . . 6  |-  x  e. 
_V
8 tfinds2.5 . . . . . . . 8  |-  ( y  e.  On  ->  ( ta  ->  ( ch  ->  th ) ) )
98a2d 26 . . . . . . 7  |-  ( y  e.  On  ->  (
( ta  ->  ch )  ->  ( ta  ->  th ) ) )
109sbcth 3341 . . . . . 6  |-  ( x  e.  _V  ->  [. x  /  y ]. (
y  e.  On  ->  ( ( ta  ->  ch )  ->  ( ta  ->  th ) ) ) )
117, 10ax-mp 5 . . . . 5  |-  [. x  /  y ]. (
y  e.  On  ->  ( ( ta  ->  ch )  ->  ( ta  ->  th ) ) )
12 sbcimg 3368 . . . . . 6  |-  ( x  e.  _V  ->  ( [. x  /  y ]. ( y  e.  On  ->  ( ( ta  ->  ch )  ->  ( ta  ->  th ) ) )  <-> 
( [. x  /  y ]. y  e.  On  ->  [. x  /  y ]. ( ( ta  ->  ch )  ->  ( ta  ->  th ) ) ) ) )
137, 12ax-mp 5 . . . . 5  |-  ( [. x  /  y ]. (
y  e.  On  ->  ( ( ta  ->  ch )  ->  ( ta  ->  th ) ) )  <->  ( [. x  /  y ]. y  e.  On  ->  [. x  / 
y ]. ( ( ta 
->  ch )  ->  ( ta  ->  th ) ) ) )
1411, 13mpbi 208 . . . 4  |-  ( [. x  /  y ]. y  e.  On  ->  [. x  / 
y ]. ( ( ta 
->  ch )  ->  ( ta  ->  th ) ) )
15 sbcel1v 3391 . . . 4  |-  ( [. x  /  y ]. y  e.  On  <->  x  e.  On )
16 sbcimg 3368 . . . . 5  |-  ( x  e.  _V  ->  ( [. x  /  y ]. ( ( ta  ->  ch )  ->  ( ta  ->  th ) )  <->  ( [. x  /  y ]. ( ta  ->  ch )  ->  [. x  /  y ]. ( ta  ->  th )
) ) )
177, 16ax-mp 5 . . . 4  |-  ( [. x  /  y ]. (
( ta  ->  ch )  ->  ( ta  ->  th ) )  <->  ( [. x  /  y ]. ( ta  ->  ch )  ->  [. x  /  y ]. ( ta  ->  th )
) )
1814, 15, 173imtr3i 265 . . 3  |-  ( x  e.  On  ->  ( [. x  /  y ]. ( ta  ->  ch )  ->  [. x  /  y ]. ( ta  ->  th )
) )
19 tfinds2.2 . . . . . . 7  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
2019bicomd 201 . . . . . 6  |-  ( x  =  y  ->  ( ch 
<-> 
ph ) )
2120equcoms 1739 . . . . 5  |-  ( y  =  x  ->  ( ch 
<-> 
ph ) )
2221imbi2d 316 . . . 4  |-  ( y  =  x  ->  (
( ta  ->  ch ) 
<->  ( ta  ->  ph )
) )
237, 22sbcie 3361 . . 3  |-  ( [. x  /  y ]. ( ta  ->  ch )  <->  ( ta  ->  ph ) )
24 vex 3111 . . . . . . 7  |-  y  e. 
_V
2524sucex 6619 . . . . . 6  |-  suc  y  e.  _V
26 tfinds2.3 . . . . . . 7  |-  ( x  =  suc  y  -> 
( ph  <->  th ) )
2726imbi2d 316 . . . . . 6  |-  ( x  =  suc  y  -> 
( ( ta  ->  ph )  <->  ( ta  ->  th ) ) )
2825, 27sbcie 3361 . . . . 5  |-  ( [. suc  y  /  x ]. ( ta  ->  ph )  <->  ( ta  ->  th )
)
2928sbcbii 3386 . . . 4  |-  ( [. x  /  y ]. [. suc  y  /  x ]. ( ta  ->  ph )  <->  [. x  / 
y ]. ( ta  ->  th ) )
30 suceq 4938 . . . . 5  |-  ( x  =  y  ->  suc  x  =  suc  y )
3130sbcco2 3350 . . . 4  |-  ( [. x  /  y ]. [. suc  y  /  x ]. ( ta  ->  ph )  <->  [. suc  x  /  x ]. ( ta 
->  ph ) )
3229, 31bitr3i 251 . . 3  |-  ( [. x  /  y ]. ( ta  ->  th )  <->  [. suc  x  /  x ]. ( ta 
->  ph ) )
3318, 23, 323imtr3g 269 . 2  |-  ( x  e.  On  ->  (
( ta  ->  ph )  ->  [. suc  x  /  x ]. ( ta  ->  ph ) ) )
34 sbsbc 3330 . . . 4  |-  ( [ y  /  x ] A. y  e.  x  ( ta  ->  ch )  <->  [. y  /  x ]. A. y  e.  x  ( ta  ->  ch )
)
3522sbralie 3096 . . . 4  |-  ( [ y  /  x ] A. y  e.  x  ( ta  ->  ch )  <->  A. x  e.  y  ( ta  ->  ph ) )
3634, 35bitr3i 251 . . 3  |-  ( [. y  /  x ]. A. y  e.  x  ( ta  ->  ch )  <->  A. x  e.  y  ( ta  ->  ph ) )
37 r19.21v 2864 . . . . . . . 8  |-  ( A. y  e.  x  ( ta  ->  ch )  <->  ( ta  ->  A. y  e.  x  ch ) )
38 tfinds2.6 . . . . . . . . 9  |-  ( Lim  x  ->  ( ta  ->  ( A. y  e.  x  ch  ->  ph )
) )
3938a2d 26 . . . . . . . 8  |-  ( Lim  x  ->  ( ( ta  ->  A. y  e.  x  ch )  ->  ( ta 
->  ph ) ) )
4037, 39syl5bi 217 . . . . . . 7  |-  ( Lim  x  ->  ( A. y  e.  x  ( ta  ->  ch )  -> 
( ta  ->  ph )
) )
4140sbcth 3341 . . . . . 6  |-  ( y  e.  _V  ->  [. y  /  x ]. ( Lim  x  ->  ( A. y  e.  x  ( ta  ->  ch )  -> 
( ta  ->  ph )
) ) )
4224, 41ax-mp 5 . . . . 5  |-  [. y  /  x ]. ( Lim  x  ->  ( A. y  e.  x  ( ta  ->  ch )  -> 
( ta  ->  ph )
) )
43 sbcimg 3368 . . . . . 6  |-  ( y  e.  _V  ->  ( [. y  /  x ]. ( Lim  x  -> 
( A. y  e.  x  ( ta  ->  ch )  ->  ( ta  ->  ph ) ) )  <-> 
( [. y  /  x ]. Lim  x  ->  [. y  /  x ]. ( A. y  e.  x  ( ta  ->  ch )  -> 
( ta  ->  ph )
) ) ) )
4424, 43ax-mp 5 . . . . 5  |-  ( [. y  /  x ]. ( Lim  x  ->  ( A. y  e.  x  ( ta  ->  ch )  -> 
( ta  ->  ph )
) )  <->  ( [. y  /  x ]. Lim  x  ->  [. y  /  x ]. ( A. y  e.  x  ( ta  ->  ch )  ->  ( ta  ->  ph ) ) ) )
4542, 44mpbi 208 . . . 4  |-  ( [. y  /  x ]. Lim  x  ->  [. y  /  x ]. ( A. y  e.  x  ( ta  ->  ch )  ->  ( ta  ->  ph ) ) )
46 limeq 4885 . . . . 5  |-  ( x  =  y  ->  ( Lim  x  <->  Lim  y ) )
4724, 46sbcie 3361 . . . 4  |-  ( [. y  /  x ]. Lim  x 
<->  Lim  y )
48 sbcimg 3368 . . . . 5  |-  ( y  e.  _V  ->  ( [. y  /  x ]. ( A. y  e.  x  ( ta  ->  ch )  ->  ( ta  ->  ph ) )  <->  ( [. y  /  x ]. A. y  e.  x  ( ta  ->  ch )  ->  [. y  /  x ]. ( ta  ->  ph )
) ) )
4924, 48ax-mp 5 . . . 4  |-  ( [. y  /  x ]. ( A. y  e.  x  ( ta  ->  ch )  ->  ( ta  ->  ph )
)  <->  ( [. y  /  x ]. A. y  e.  x  ( ta  ->  ch )  ->  [. y  /  x ]. ( ta 
->  ph ) ) )
5045, 47, 493imtr3i 265 . . 3  |-  ( Lim  y  ->  ( [. y  /  x ]. A. y  e.  x  ( ta  ->  ch )  ->  [. y  /  x ]. ( ta  ->  ph )
) )
5136, 50syl5bir 218 . 2  |-  ( Lim  y  ->  ( A. x  e.  y  ( ta  ->  ph )  ->  [. y  /  x ]. ( ta 
->  ph ) ) )
526, 33, 51tfindes 6670 1  |-  ( x  e.  On  ->  ( ta  ->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1374   [wsb 1706    e. wcel 1762   A.wral 2809   _Vcvv 3108   [.wsbc 3326   (/)c0 3780   Oncon0 4873   Lim wlim 4874   suc csuc 4875
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pr 4681  ax-un 6569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-sbc 3327  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3781  df-if 3935  df-pw 4007  df-sn 4023  df-pr 4025  df-tp 4027  df-op 4029  df-uni 4241  df-br 4443  df-opab 4501  df-tr 4536  df-eprel 4786  df-po 4795  df-so 4796  df-fr 4833  df-we 4835  df-ord 4876  df-on 4877  df-lim 4878  df-suc 4879
This theorem is referenced by:  inar1  9144  grur1a  9188
  Copyright terms: Public domain W3C validator