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

Theorem tfindsg2 4841
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 hypothesis for successors, and the induction hypothesis 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 4606 . . 3  |-  ( ( A  e.  On  /\  B  e.  A )  ->  B  e.  On )
2 sucelon 4797 . . 3  |-  ( B  e.  On  <->  suc  B  e.  On )
31, 2sylib 189 . 2  |-  ( ( A  e.  On  /\  B  e.  A )  ->  suc  B  e.  On )
4 eloni 4591 . . . 4  |-  ( A  e.  On  ->  Ord  A )
5 ordsucss 4798 . . . 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 419 . 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 205 . . . . 5  |-  ( suc 
B  e.  On  ->  ps )
14 eloni 4591 . . . . . . . . . 10  |-  ( y  e.  On  ->  Ord  y )
15 ordelsuc 4800 . . . . . . . . . 10  |-  ( ( B  e.  On  /\  Ord  y )  ->  ( B  e.  y  <->  suc  B  C_  y ) )
1614, 15sylan2 461 . . . . . . . . 9  |-  ( ( B  e.  On  /\  y  e.  On )  ->  ( B  e.  y  <->  suc  B  C_  y )
)
1716ancoms 440 . . . . . . . 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 424 . . . . . . . . 9  |-  ( y  e.  On  ->  ( B  e.  y  ->  ( ch  ->  th )
) )
2019adantr 452 . . . . . . . 8  |-  ( ( y  e.  On  /\  B  e.  On )  ->  ( B  e.  y  ->  ( ch  ->  th ) ) )
2117, 20sylbird 227 . . . . . . 7  |-  ( ( y  e.  On  /\  B  e.  On )  ->  ( suc  B  C_  y  ->  ( ch  ->  th ) ) )
222, 21sylan2br 463 . . . . . 6  |-  ( ( y  e.  On  /\  suc  B  e.  On )  ->  ( suc  B  C_  y  ->  ( ch  ->  th ) ) )
2322imp 419 . . . . 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 424 . . . . . . . . 9  |-  ( Lim  x  ->  ( B  e.  x  ->  ( A. y  e.  x  ( B  e.  y  ->  ch )  ->  ph ) ) )
2625adantr 452 . . . . . . . 8  |-  ( ( Lim  x  /\  B  e.  On )  ->  ( B  e.  x  ->  ( A. y  e.  x  ( B  e.  y  ->  ch )  ->  ph )
) )
27 vex 2959 . . . . . . . . . . 11  |-  x  e. 
_V
28 limelon 4644 . . . . . . . . . . 11  |-  ( ( x  e.  _V  /\  Lim  x )  ->  x  e.  On )
2927, 28mpan 652 . . . . . . . . . 10  |-  ( Lim  x  ->  x  e.  On )
30 eloni 4591 . . . . . . . . . . . 12  |-  ( x  e.  On  ->  Ord  x )
31 ordelsuc 4800 . . . . . . . . . . . 12  |-  ( ( B  e.  On  /\  Ord  x )  ->  ( B  e.  x  <->  suc  B  C_  x ) )
3230, 31sylan2 461 . . . . . . . . . . 11  |-  ( ( B  e.  On  /\  x  e.  On )  ->  ( B  e.  x  <->  suc 
B  C_  x )
)
33 onelon 4606 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  On  /\  y  e.  x )  ->  y  e.  On )
3433, 14syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  On  /\  y  e.  x )  ->  Ord  y )
3534, 15sylan2 461 . . . . . . . . . . . . . . 15  |-  ( ( B  e.  On  /\  ( x  e.  On  /\  y  e.  x ) )  ->  ( B  e.  y  <->  suc  B  C_  y
) )
3635anassrs 630 . . . . . . . . . . . . . 14  |-  ( ( ( B  e.  On  /\  x  e.  On )  /\  y  e.  x
)  ->  ( B  e.  y  <->  suc  B  C_  y
) )
3736imbi1d 309 . . . . . . . . . . . . 13  |-  ( ( ( B  e.  On  /\  x  e.  On )  /\  y  e.  x
)  ->  ( ( B  e.  y  ->  ch )  <->  ( suc  B  C_  y  ->  ch )
) )
3837ralbidva 2721 . . . . . . . . . . . 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 309 . . . . . . . . . . 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 312 . . . . . . . . . 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 461 . . . . . . . . 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 440 . . . . . . . 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 202 . . . . . . 7  |-  ( ( Lim  x  /\  B  e.  On )  ->  ( suc  B  C_  x  ->  ( A. y  e.  x  ( suc  B  C_  y  ->  ch )  ->  ph )
) )
442, 43sylan2br 463 . . . . . 6  |-  ( ( Lim  x  /\  suc  B  e.  On )  -> 
( suc  B  C_  x  ->  ( A. y  e.  x  ( suc  B  C_  y  ->  ch )  ->  ph ) ) )
4544imp 419 . . . . 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 4840 . . . 4  |-  ( ( ( A  e.  On  /\ 
suc  B  e.  On )  /\  suc  B  C_  A )  ->  ta )
4746expl 602 . . 3  |-  ( A  e.  On  ->  (
( suc  B  e.  On  /\  suc  B  C_  A )  ->  ta ) )
4847adantr 452 . 2  |-  ( ( A  e.  On  /\  B  e.  A )  ->  ( ( suc  B  e.  On  /\  suc  B  C_  A )  ->  ta ) )
493, 7, 48mp2and 661 1  |-  ( ( A  e.  On  /\  B  e.  A )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652    e. wcel 1725   A.wral 2705   _Vcvv 2956    C_ wss 3320   Ord word 4580   Oncon0 4581   Lim wlim 4582   suc csuc 4583
This theorem is referenced by:  oeordi  6830
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 4330  ax-nul 4338  ax-pr 4403  ax-un 4701
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 2710  df-rex 2711  df-rab 2714  df-v 2958  df-sbc 3162  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-tp 3822  df-op 3823  df-uni 4016  df-br 4213  df-opab 4267  df-tr 4303  df-eprel 4494  df-po 4503  df-so 4504  df-fr 4541  df-we 4543  df-ord 4584  df-on 4585  df-lim 4586  df-suc 4587
  Copyright terms: Public domain W3C validator