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

Theorem tfindsg2 6691
Description: Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. The basis of this version is an arbitrary ordinal  suc  B instead of zero. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 5-Jan-2005.)
Hypotheses
Ref Expression
tfindsg2.1  |-  ( x  =  suc  B  -> 
( ph  <->  ps ) )
tfindsg2.2  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
tfindsg2.3  |-  ( x  =  suc  y  -> 
( ph  <->  th ) )
tfindsg2.4  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
tfindsg2.5  |-  ( B  e.  On  ->  ps )
tfindsg2.6  |-  ( ( y  e.  On  /\  B  e.  y )  ->  ( ch  ->  th )
)
tfindsg2.7  |-  ( ( Lim  x  /\  B  e.  x )  ->  ( A. y  e.  x  ( B  e.  y  ->  ch )  ->  ph )
)
Assertion
Ref Expression
tfindsg2  |-  ( ( A  e.  On  /\  B  e.  A )  ->  ta )
Distinct variable groups:    x, A    x, y, B    ch, x    th, x    ta, x    ph, y
Allowed substitution hints:    ph( x)    ps( x, y)    ch( y)    th( y)    ta( y)    A( y)

Proof of Theorem tfindsg2
StepHypRef Expression
1 onelon 4909 . . 3  |-  ( ( A  e.  On  /\  B  e.  A )  ->  B  e.  On )
2 sucelon 6647 . . 3  |-  ( B  e.  On  <->  suc  B  e.  On )
31, 2sylib 196 . 2  |-  ( ( A  e.  On  /\  B  e.  A )  ->  suc  B  e.  On )
4 eloni 4894 . . . 4  |-  ( A  e.  On  ->  Ord  A )
5 ordsucss 6648 . . . 4  |-  ( Ord 
A  ->  ( B  e.  A  ->  suc  B  C_  A ) )
64, 5syl 16 . . 3  |-  ( A  e.  On  ->  ( B  e.  A  ->  suc 
B  C_  A )
)
76imp 429 . 2  |-  ( ( A  e.  On  /\  B  e.  A )  ->  suc  B  C_  A
)
8 tfindsg2.1 . . . . 5  |-  ( x  =  suc  B  -> 
( ph  <->  ps ) )
9 tfindsg2.2 . . . . 5  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
10 tfindsg2.3 . . . . 5  |-  ( x  =  suc  y  -> 
( ph  <->  th ) )
11 tfindsg2.4 . . . . 5  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
12 tfindsg2.5 . . . . . 6  |-  ( B  e.  On  ->  ps )
132, 12sylbir 213 . . . . 5  |-  ( suc 
B  e.  On  ->  ps )
14 eloni 4894 . . . . . . . . . 10  |-  ( y  e.  On  ->  Ord  y )
15 ordelsuc 6650 . . . . . . . . . 10  |-  ( ( B  e.  On  /\  Ord  y )  ->  ( B  e.  y  <->  suc  B  C_  y ) )
1614, 15sylan2 474 . . . . . . . . 9  |-  ( ( B  e.  On  /\  y  e.  On )  ->  ( B  e.  y  <->  suc  B  C_  y )
)
1716ancoms 453 . . . . . . . 8  |-  ( ( y  e.  On  /\  B  e.  On )  ->  ( B  e.  y  <->  suc  B  C_  y )
)
18 tfindsg2.6 . . . . . . . . . 10  |-  ( ( y  e.  On  /\  B  e.  y )  ->  ( ch  ->  th )
)
1918ex 434 . . . . . . . . 9  |-  ( y  e.  On  ->  ( B  e.  y  ->  ( ch  ->  th )
) )
2019adantr 465 . . . . . . . 8  |-  ( ( y  e.  On  /\  B  e.  On )  ->  ( B  e.  y  ->  ( ch  ->  th ) ) )
2117, 20sylbird 235 . . . . . . 7  |-  ( ( y  e.  On  /\  B  e.  On )  ->  ( suc  B  C_  y  ->  ( ch  ->  th ) ) )
222, 21sylan2br 476 . . . . . 6  |-  ( ( y  e.  On  /\  suc  B  e.  On )  ->  ( suc  B  C_  y  ->  ( ch  ->  th ) ) )
2322imp 429 . . . . 5  |-  ( ( ( y  e.  On  /\ 
suc  B  e.  On )  /\  suc  B  C_  y )  ->  ( ch  ->  th ) )
24 tfindsg2.7 . . . . . . . . . 10  |-  ( ( Lim  x  /\  B  e.  x )  ->  ( A. y  e.  x  ( B  e.  y  ->  ch )  ->  ph )
)
2524ex 434 . . . . . . . . 9  |-  ( Lim  x  ->  ( B  e.  x  ->  ( A. y  e.  x  ( B  e.  y  ->  ch )  ->  ph ) ) )
2625adantr 465 . . . . . . . 8  |-  ( ( Lim  x  /\  B  e.  On )  ->  ( B  e.  x  ->  ( A. y  e.  x  ( B  e.  y  ->  ch )  ->  ph )
) )
27 vex 3121 . . . . . . . . . . 11  |-  x  e. 
_V
28 limelon 4947 . . . . . . . . . . 11  |-  ( ( x  e.  _V  /\  Lim  x )  ->  x  e.  On )
2927, 28mpan 670 . . . . . . . . . 10  |-  ( Lim  x  ->  x  e.  On )
30 eloni 4894 . . . . . . . . . . . 12  |-  ( x  e.  On  ->  Ord  x )
31 ordelsuc 6650 . . . . . . . . . . . 12  |-  ( ( B  e.  On  /\  Ord  x )  ->  ( B  e.  x  <->  suc  B  C_  x ) )
3230, 31sylan2 474 . . . . . . . . . . 11  |-  ( ( B  e.  On  /\  x  e.  On )  ->  ( B  e.  x  <->  suc 
B  C_  x )
)
33 onelon 4909 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  On  /\  y  e.  x )  ->  y  e.  On )
3433, 14syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  On  /\  y  e.  x )  ->  Ord  y )
3534, 15sylan2 474 . . . . . . . . . . . . . . 15  |-  ( ( B  e.  On  /\  ( x  e.  On  /\  y  e.  x ) )  ->  ( B  e.  y  <->  suc  B  C_  y
) )
3635anassrs 648 . . . . . . . . . . . . . 14  |-  ( ( ( B  e.  On  /\  x  e.  On )  /\  y  e.  x
)  ->  ( B  e.  y  <->  suc  B  C_  y
) )
3736imbi1d 317 . . . . . . . . . . . . 13  |-  ( ( ( B  e.  On  /\  x  e.  On )  /\  y  e.  x
)  ->  ( ( B  e.  y  ->  ch )  <->  ( suc  B  C_  y  ->  ch )
) )
3837ralbidva 2903 . . . . . . . . . . . 12  |-  ( ( B  e.  On  /\  x  e.  On )  ->  ( A. y  e.  x  ( B  e.  y  ->  ch )  <->  A. y  e.  x  ( suc  B  C_  y  ->  ch ) ) )
3938imbi1d 317 . . . . . . . . . . 11  |-  ( ( B  e.  On  /\  x  e.  On )  ->  ( ( A. y  e.  x  ( B  e.  y  ->  ch )  ->  ph )  <->  ( A. y  e.  x  ( suc  B  C_  y  ->  ch )  ->  ph ) ) )
4032, 39imbi12d 320 . . . . . . . . . 10  |-  ( ( B  e.  On  /\  x  e.  On )  ->  ( ( B  e.  x  ->  ( A. y  e.  x  ( B  e.  y  ->  ch )  ->  ph ) )  <-> 
( suc  B  C_  x  ->  ( A. y  e.  x  ( suc  B  C_  y  ->  ch )  ->  ph ) ) ) )
4129, 40sylan2 474 . . . . . . . . 9  |-  ( ( B  e.  On  /\  Lim  x )  ->  (
( B  e.  x  ->  ( A. y  e.  x  ( B  e.  y  ->  ch )  ->  ph ) )  <->  ( suc  B 
C_  x  ->  ( A. y  e.  x  ( suc  B  C_  y  ->  ch )  ->  ph )
) ) )
4241ancoms 453 . . . . . . . 8  |-  ( ( Lim  x  /\  B  e.  On )  ->  (
( B  e.  x  ->  ( A. y  e.  x  ( B  e.  y  ->  ch )  ->  ph ) )  <->  ( suc  B 
C_  x  ->  ( A. y  e.  x  ( suc  B  C_  y  ->  ch )  ->  ph )
) ) )
4326, 42mpbid 210 . . . . . . 7  |-  ( ( Lim  x  /\  B  e.  On )  ->  ( suc  B  C_  x  ->  ( A. y  e.  x  ( suc  B  C_  y  ->  ch )  ->  ph )
) )
442, 43sylan2br 476 . . . . . 6  |-  ( ( Lim  x  /\  suc  B  e.  On )  -> 
( suc  B  C_  x  ->  ( A. y  e.  x  ( suc  B  C_  y  ->  ch )  ->  ph ) ) )
4544imp 429 . . . . 5  |-  ( ( ( Lim  x  /\  suc  B  e.  On )  /\  suc  B  C_  x )  ->  ( A. y  e.  x  ( suc  B  C_  y  ->  ch )  ->  ph )
)
468, 9, 10, 11, 13, 23, 45tfindsg 6690 . . . 4  |-  ( ( ( A  e.  On  /\ 
suc  B  e.  On )  /\  suc  B  C_  A )  ->  ta )
4746expl 618 . . 3  |-  ( A  e.  On  ->  (
( suc  B  e.  On  /\  suc  B  C_  A )  ->  ta ) )
4847adantr 465 . 2  |-  ( ( A  e.  On  /\  B  e.  A )  ->  ( ( suc  B  e.  On  /\  suc  B  C_  A )  ->  ta ) )
493, 7, 48mp2and 679 1  |-  ( ( A  e.  On  /\  B  e.  A )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379    e. wcel 1767   A.wral 2817   _Vcvv 3118    C_ wss 3481   Ord word 4883   Oncon0 4884   Lim wlim 4885   suc csuc 4886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pr 4692  ax-un 6587
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-tr 4547  df-eprel 4797  df-po 4806  df-so 4807  df-fr 4844  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890
This theorem is referenced by:  oeordi  7248
  Copyright terms: Public domain W3C validator