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

Theorem tfinds2 6709
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 4528 . . . 4  |-  (/)  e.  _V
3 tfinds2.1 . . . . 5  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
43imbi2d 323 . . . 4  |-  ( x  =  (/)  ->  ( ( ta  ->  ph )  <->  ( ta  ->  ps ) ) )
52, 4sbcie 3290 . . 3  |-  ( [. (/)  /  x ]. ( ta 
->  ph )  <->  ( ta  ->  ps ) )
61, 5mpbir 214 . 2  |-  [. (/)  /  x ]. ( ta  ->  ph )
7 vex 3034 . . . . . 6  |-  x  e. 
_V
8 tfinds2.5 . . . . . . . 8  |-  ( y  e.  On  ->  ( ta  ->  ( ch  ->  th ) ) )
98a2d 28 . . . . . . 7  |-  ( y  e.  On  ->  (
( ta  ->  ch )  ->  ( ta  ->  th ) ) )
109sbcth 3270 . . . . . 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 3297 . . . . . 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 213 . . . 4  |-  ( [. x  /  y ]. y  e.  On  ->  [. x  / 
y ]. ( ( ta 
->  ch )  ->  ( ta  ->  th ) ) )
15 sbcel1v 3314 . . . 4  |-  ( [. x  /  y ]. y  e.  On  <->  x  e.  On )
16 sbcimg 3297 . . . . 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 273 . . 3  |-  ( x  e.  On  ->  ( [. x  /  y ]. ( ta  ->  ch )  ->  [. x  /  y ]. ( ta  ->  th )
) )
19 tfinds2.2 . . . . . . 7  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
2019bicomd 206 . . . . . 6  |-  ( x  =  y  ->  ( ch 
<-> 
ph ) )
2120equcoms 1872 . . . . 5  |-  ( y  =  x  ->  ( ch 
<-> 
ph ) )
2221imbi2d 323 . . . 4  |-  ( y  =  x  ->  (
( ta  ->  ch ) 
<->  ( ta  ->  ph )
) )
237, 22sbcie 3290 . . 3  |-  ( [. x  /  y ]. ( ta  ->  ch )  <->  ( ta  ->  ph ) )
24 vex 3034 . . . . . . 7  |-  y  e. 
_V
2524sucex 6657 . . . . . 6  |-  suc  y  e.  _V
26 tfinds2.3 . . . . . . 7  |-  ( x  =  suc  y  -> 
( ph  <->  th ) )
2726imbi2d 323 . . . . . 6  |-  ( x  =  suc  y  -> 
( ( ta  ->  ph )  <->  ( ta  ->  th ) ) )
2825, 27sbcie 3290 . . . . 5  |-  ( [. suc  y  /  x ]. ( ta  ->  ph )  <->  ( ta  ->  th )
)
2928sbcbii 3311 . . . 4  |-  ( [. x  /  y ]. [. suc  y  /  x ]. ( ta  ->  ph )  <->  [. x  / 
y ]. ( ta  ->  th ) )
30 suceq 5495 . . . . 5  |-  ( x  =  y  ->  suc  x  =  suc  y )
3130sbcco2 3279 . . . 4  |-  ( [. x  /  y ]. [. suc  y  /  x ]. ( ta  ->  ph )  <->  [. suc  x  /  x ]. ( ta 
->  ph ) )
3229, 31bitr3i 259 . . 3  |-  ( [. x  /  y ]. ( ta  ->  th )  <->  [. suc  x  /  x ]. ( ta 
->  ph ) )
3318, 23, 323imtr3g 277 . 2  |-  ( x  e.  On  ->  (
( ta  ->  ph )  ->  [. suc  x  /  x ]. ( ta  ->  ph ) ) )
34 sbsbc 3259 . . . 4  |-  ( [ y  /  x ] A. y  e.  x  ( ta  ->  ch )  <->  [. y  /  x ]. A. y  e.  x  ( ta  ->  ch )
)
3522sbralie 3018 . . . 4  |-  ( [ y  /  x ] A. y  e.  x  ( ta  ->  ch )  <->  A. x  e.  y  ( ta  ->  ph ) )
3634, 35bitr3i 259 . . 3  |-  ( [. y  /  x ]. A. y  e.  x  ( ta  ->  ch )  <->  A. x  e.  y  ( ta  ->  ph ) )
37 r19.21v 2803 . . . . . . . 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 28 . . . . . . . 8  |-  ( Lim  x  ->  ( ( ta  ->  A. y  e.  x  ch )  ->  ( ta 
->  ph ) ) )
4037, 39syl5bi 225 . . . . . . 7  |-  ( Lim  x  ->  ( A. y  e.  x  ( ta  ->  ch )  -> 
( ta  ->  ph )
) )
4140sbcth 3270 . . . . . 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 3297 . . . . . 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 213 . . . 4  |-  ( [. y  /  x ]. Lim  x  ->  [. y  /  x ]. ( A. y  e.  x  ( ta  ->  ch )  ->  ( ta  ->  ph ) ) )
46 limeq 5442 . . . . 5  |-  ( x  =  y  ->  ( Lim  x  <->  Lim  y ) )
4724, 46sbcie 3290 . . . 4  |-  ( [. y  /  x ]. Lim  x 
<->  Lim  y )
48 sbcimg 3297 . . . . 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 273 . . 3  |-  ( Lim  y  ->  ( [. y  /  x ]. A. y  e.  x  ( ta  ->  ch )  ->  [. y  /  x ]. ( ta  ->  ph )
) )
5136, 50syl5bir 226 . 2  |-  ( Lim  y  ->  ( A. x  e.  y  ( ta  ->  ph )  ->  [. y  /  x ]. ( ta 
->  ph ) ) )
526, 33, 51tfindes 6708 1  |-  ( x  e.  On  ->  ( ta  ->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1452   [wsb 1805    e. wcel 1904   A.wral 2756   _Vcvv 3031   [.wsbc 3255   (/)c0 3722   Oncon0 5430   Lim wlim 5431   suc csuc 5432
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639  ax-un 6602
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-tr 4491  df-eprel 4750  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436
This theorem is referenced by:  inar1  9218  grur1a  9262
  Copyright terms: Public domain W3C validator