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

Theorem tfindsg2 6467
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 4739 . . 3  |-  ( ( A  e.  On  /\  B  e.  A )  ->  B  e.  On )
2 sucelon 6423 . . 3  |-  ( B  e.  On  <->  suc  B  e.  On )
31, 2sylib 196 . 2  |-  ( ( A  e.  On  /\  B  e.  A )  ->  suc  B  e.  On )
4 eloni 4724 . . . 4  |-  ( A  e.  On  ->  Ord  A )
5 ordsucss 6424 . . . 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 4724 . . . . . . . . . 10  |-  ( y  e.  On  ->  Ord  y )
15 ordelsuc 6426 . . . . . . . . . 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 2970 . . . . . . . . . . 11  |-  x  e. 
_V
28 limelon 4777 . . . . . . . . . . 11  |-  ( ( x  e.  _V  /\  Lim  x )  ->  x  e.  On )
2927, 28mpan 670 . . . . . . . . . 10  |-  ( Lim  x  ->  x  e.  On )
30 eloni 4724 . . . . . . . . . . . 12  |-  ( x  e.  On  ->  Ord  x )
31 ordelsuc 6426 . . . . . . . . . . . 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 4739 . . . . . . . . . . . . . . . . 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 2726 . . . . . . . . . . . 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 6466 . . . 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 1369    e. wcel 1756   A.wral 2710   _Vcvv 2967    C_ wss 3323   Ord word 4713   Oncon0 4714   Lim wlim 4715   suc csuc 4716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-tr 4381  df-eprel 4627  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720
This theorem is referenced by:  oeordi  7018
  Copyright terms: Public domain W3C validator