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

Theorem tfindsg 4623
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  B instead of zero. Remark in [TakeutiZaring] p. 57. (Contributed by NM, 5-Mar-2004.)
Hypotheses
Ref Expression
tfindsg.1  |-  ( x  =  B  ->  ( ph 
<->  ps ) )
tfindsg.2  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
tfindsg.3  |-  ( x  =  suc  y  -> 
( ph  <->  th ) )
tfindsg.4  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
tfindsg.5  |-  ( B  e.  On  ->  ps )
tfindsg.6  |-  ( ( ( y  e.  On  /\  B  e.  On )  /\  B  C_  y
)  ->  ( ch  ->  th ) )
tfindsg.7  |-  ( ( ( Lim  x  /\  B  e.  On )  /\  B  C_  x )  ->  ( A. y  e.  x  ( B  C_  y  ->  ch )  ->  ph ) )
Assertion
Ref Expression
tfindsg  |-  ( ( ( A  e.  On  /\  B  e.  On )  /\  B  C_  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 tfindsg
StepHypRef Expression
1 sseq2 3175 . . . . . . 7  |-  ( x  =  (/)  ->  ( B 
C_  x  <->  B  C_  (/) ) )
21adantl 454 . . . . . 6  |-  ( ( B  =  (/)  /\  x  =  (/) )  ->  ( B  C_  x  <->  B  C_  (/) ) )
3 eqeq2 2267 . . . . . . . 8  |-  ( B  =  (/)  ->  ( x  =  B  <->  x  =  (/) ) )
4 tfindsg.1 . . . . . . . 8  |-  ( x  =  B  ->  ( ph 
<->  ps ) )
53, 4syl6bir 222 . . . . . . 7  |-  ( B  =  (/)  ->  ( x  =  (/)  ->  ( ph  <->  ps ) ) )
65imp 420 . . . . . 6  |-  ( ( B  =  (/)  /\  x  =  (/) )  ->  ( ph 
<->  ps ) )
72, 6imbi12d 313 . . . . 5  |-  ( ( B  =  (/)  /\  x  =  (/) )  ->  (
( B  C_  x  ->  ph )  <->  ( B  C_  (/)  ->  ps ) ) )
81imbi1d 310 . . . . . 6  |-  ( x  =  (/)  ->  ( ( B  C_  x  ->  ph )  <->  ( B  C_  (/) 
->  ph ) ) )
9 ss0 3460 . . . . . . . . 9  |-  ( B 
C_  (/)  ->  B  =  (/) )
109con3i 129 . . . . . . . 8  |-  ( -.  B  =  (/)  ->  -.  B  C_  (/) )
1110pm2.21d 100 . . . . . . 7  |-  ( -.  B  =  (/)  ->  ( B  C_  (/)  ->  ( ph  <->  ps ) ) )
1211pm5.74d 240 . . . . . 6  |-  ( -.  B  =  (/)  ->  (
( B  C_  (/)  ->  ph )  <->  ( B  C_  (/)  ->  ps ) ) )
138, 12sylan9bbr 684 . . . . 5  |-  ( ( -.  B  =  (/)  /\  x  =  (/) )  -> 
( ( B  C_  x  ->  ph )  <->  ( B  C_  (/)  ->  ps ) ) )
147, 13pm2.61ian 768 . . . 4  |-  ( x  =  (/)  ->  ( ( B  C_  x  ->  ph )  <->  ( B  C_  (/) 
->  ps ) ) )
1514imbi2d 309 . . 3  |-  ( x  =  (/)  ->  ( ( B  e.  On  ->  ( B  C_  x  ->  ph ) )  <->  ( B  e.  On  ->  ( B  C_  (/)  ->  ps ) ) ) )
16 sseq2 3175 . . . . 5  |-  ( x  =  y  ->  ( B  C_  x  <->  B  C_  y
) )
17 tfindsg.2 . . . . 5  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
1816, 17imbi12d 313 . . . 4  |-  ( x  =  y  ->  (
( B  C_  x  ->  ph )  <->  ( B  C_  y  ->  ch )
) )
1918imbi2d 309 . . 3  |-  ( x  =  y  ->  (
( B  e.  On  ->  ( B  C_  x  ->  ph ) )  <->  ( B  e.  On  ->  ( B  C_  y  ->  ch )
) ) )
20 sseq2 3175 . . . . 5  |-  ( x  =  suc  y  -> 
( B  C_  x  <->  B 
C_  suc  y )
)
21 tfindsg.3 . . . . 5  |-  ( x  =  suc  y  -> 
( ph  <->  th ) )
2220, 21imbi12d 313 . . . 4  |-  ( x  =  suc  y  -> 
( ( B  C_  x  ->  ph )  <->  ( B  C_ 
suc  y  ->  th )
) )
2322imbi2d 309 . . 3  |-  ( x  =  suc  y  -> 
( ( B  e.  On  ->  ( B  C_  x  ->  ph ) )  <-> 
( B  e.  On  ->  ( B  C_  suc  y  ->  th ) ) ) )
24 sseq2 3175 . . . . 5  |-  ( x  =  A  ->  ( B  C_  x  <->  B  C_  A
) )
25 tfindsg.4 . . . . 5  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
2624, 25imbi12d 313 . . . 4  |-  ( x  =  A  ->  (
( B  C_  x  ->  ph )  <->  ( B  C_  A  ->  ta )
) )
2726imbi2d 309 . . 3  |-  ( x  =  A  ->  (
( B  e.  On  ->  ( B  C_  x  ->  ph ) )  <->  ( B  e.  On  ->  ( B  C_  A  ->  ta )
) ) )
28 tfindsg.5 . . . 4  |-  ( B  e.  On  ->  ps )
2928a1d 24 . . 3  |-  ( B  e.  On  ->  ( B  C_  (/)  ->  ps )
)
30 vex 2766 . . . . . . . . . . . . . 14  |-  y  e. 
_V
3130sucex 4574 . . . . . . . . . . . . 13  |-  suc  y  e.  _V
3231eqvinc 2870 . . . . . . . . . . . 12  |-  ( suc  y  =  B  <->  E. x
( x  =  suc  y  /\  x  =  B ) )
3328, 4syl5ibr 214 . . . . . . . . . . . . . 14  |-  ( x  =  B  ->  ( B  e.  On  ->  ph ) )
3421biimpd 200 . . . . . . . . . . . . . 14  |-  ( x  =  suc  y  -> 
( ph  ->  th )
)
3533, 34sylan9r 642 . . . . . . . . . . . . 13  |-  ( ( x  =  suc  y  /\  x  =  B
)  ->  ( B  e.  On  ->  th )
)
3635exlimiv 2024 . . . . . . . . . . . 12  |-  ( E. x ( x  =  suc  y  /\  x  =  B )  ->  ( B  e.  On  ->  th ) )
3732, 36sylbi 189 . . . . . . . . . . 11  |-  ( suc  y  =  B  -> 
( B  e.  On  ->  th ) )
3837eqcoms 2261 . . . . . . . . . 10  |-  ( B  =  suc  y  -> 
( B  e.  On  ->  th ) )
3938imim2i 15 . . . . . . . . 9  |-  ( ( B  C_  suc  y  ->  B  =  suc  y )  ->  ( B  C_  suc  y  ->  ( B  e.  On  ->  th )
) )
4039a1d 24 . . . . . . . 8  |-  ( ( B  C_  suc  y  ->  B  =  suc  y )  ->  ( ( B 
C_  y  ->  ch )  ->  ( B  C_  suc  y  ->  ( B  e.  On  ->  th )
) ) )
4140com4r 82 . . . . . . 7  |-  ( B  e.  On  ->  (
( B  C_  suc  y  ->  B  =  suc  y )  ->  (
( B  C_  y  ->  ch )  ->  ( B  C_  suc  y  ->  th ) ) ) )
4241adantl 454 . . . . . 6  |-  ( ( y  e.  On  /\  B  e.  On )  ->  ( ( B  C_  suc  y  ->  B  =  suc  y )  -> 
( ( B  C_  y  ->  ch )  -> 
( B  C_  suc  y  ->  th ) ) ) )
43 df-ne 2423 . . . . . . . . 9  |-  ( B  =/=  suc  y  <->  -.  B  =  suc  y )
4443anbi2i 678 . . . . . . . 8  |-  ( ( B  C_  suc  y  /\  B  =/=  suc  y )  <->  ( B  C_  suc  y  /\  -.  B  =  suc  y ) )
45 annim 416 . . . . . . . 8  |-  ( ( B  C_  suc  y  /\  -.  B  =  suc  y )  <->  -.  ( B  C_  suc  y  ->  B  =  suc  y ) )
4644, 45bitri 242 . . . . . . 7  |-  ( ( B  C_  suc  y  /\  B  =/=  suc  y )  <->  -.  ( B  C_  suc  y  ->  B  =  suc  y ) )
47 onsssuc 4452 . . . . . . . . . 10  |-  ( ( B  e.  On  /\  y  e.  On )  ->  ( B  C_  y  <->  B  e.  suc  y ) )
48 suceloni 4576 . . . . . . . . . . 11  |-  ( y  e.  On  ->  suc  y  e.  On )
49 onelpss 4404 . . . . . . . . . . 11  |-  ( ( B  e.  On  /\  suc  y  e.  On )  ->  ( B  e. 
suc  y  <->  ( B  C_ 
suc  y  /\  B  =/=  suc  y ) ) )
5048, 49sylan2 462 . . . . . . . . . 10  |-  ( ( B  e.  On  /\  y  e.  On )  ->  ( B  e.  suc  y 
<->  ( B  C_  suc  y  /\  B  =/=  suc  y ) ) )
5147, 50bitrd 246 . . . . . . . . 9  |-  ( ( B  e.  On  /\  y  e.  On )  ->  ( B  C_  y  <->  ( B  C_  suc  y  /\  B  =/=  suc  y )
) )
5251ancoms 441 . . . . . . . 8  |-  ( ( y  e.  On  /\  B  e.  On )  ->  ( B  C_  y  <->  ( B  C_  suc  y  /\  B  =/=  suc  y )
) )
53 tfindsg.6 . . . . . . . . . . . 12  |-  ( ( ( y  e.  On  /\  B  e.  On )  /\  B  C_  y
)  ->  ( ch  ->  th ) )
5453ex 425 . . . . . . . . . . 11  |-  ( ( y  e.  On  /\  B  e.  On )  ->  ( B  C_  y  ->  ( ch  ->  th )
) )
55 ax-1 7 . . . . . . . . . . 11  |-  ( th 
->  ( B  C_  suc  y  ->  th ) )
5654, 55syl8 67 . . . . . . . . . 10  |-  ( ( y  e.  On  /\  B  e.  On )  ->  ( B  C_  y  ->  ( ch  ->  ( B  C_  suc  y  ->  th ) ) ) )
5756a2d 25 . . . . . . . . 9  |-  ( ( y  e.  On  /\  B  e.  On )  ->  ( ( B  C_  y  ->  ch )  -> 
( B  C_  y  ->  ( B  C_  suc  y  ->  th ) ) ) )
5857com23 74 . . . . . . . 8  |-  ( ( y  e.  On  /\  B  e.  On )  ->  ( B  C_  y  ->  ( ( B  C_  y  ->  ch )  -> 
( B  C_  suc  y  ->  th ) ) ) )
5952, 58sylbird 228 . . . . . . 7  |-  ( ( y  e.  On  /\  B  e.  On )  ->  ( ( B  C_  suc  y  /\  B  =/= 
suc  y )  -> 
( ( B  C_  y  ->  ch )  -> 
( B  C_  suc  y  ->  th ) ) ) )
6046, 59syl5bir 211 . . . . . 6  |-  ( ( y  e.  On  /\  B  e.  On )  ->  ( -.  ( B 
C_  suc  y  ->  B  =  suc  y )  ->  ( ( B 
C_  y  ->  ch )  ->  ( B  C_  suc  y  ->  th )
) ) )
6142, 60pm2.61d 152 . . . . 5  |-  ( ( y  e.  On  /\  B  e.  On )  ->  ( ( B  C_  y  ->  ch )  -> 
( B  C_  suc  y  ->  th ) ) )
6261ex 425 . . . 4  |-  ( y  e.  On  ->  ( B  e.  On  ->  ( ( B  C_  y  ->  ch )  ->  ( B  C_  suc  y  ->  th ) ) ) )
6362a2d 25 . . 3  |-  ( y  e.  On  ->  (
( B  e.  On  ->  ( B  C_  y  ->  ch ) )  -> 
( B  e.  On  ->  ( B  C_  suc  y  ->  th ) ) ) )
64 pm2.27 37 . . . . . . . . 9  |-  ( B  e.  On  ->  (
( B  e.  On  ->  ( B  C_  y  ->  ch ) )  -> 
( B  C_  y  ->  ch ) ) )
6564ralimdv 2597 . . . . . . . 8  |-  ( B  e.  On  ->  ( A. y  e.  x  ( B  e.  On  ->  ( B  C_  y  ->  ch ) )  ->  A. y  e.  x  ( B  C_  y  ->  ch ) ) )
6665ad2antlr 710 . . . . . . 7  |-  ( ( ( Lim  x  /\  B  e.  On )  /\  B  C_  x )  ->  ( A. y  e.  x  ( B  e.  On  ->  ( B  C_  y  ->  ch )
)  ->  A. y  e.  x  ( B  C_  y  ->  ch )
) )
67 tfindsg.7 . . . . . . 7  |-  ( ( ( Lim  x  /\  B  e.  On )  /\  B  C_  x )  ->  ( A. y  e.  x  ( B  C_  y  ->  ch )  ->  ph ) )
6866, 67syld 42 . . . . . 6  |-  ( ( ( Lim  x  /\  B  e.  On )  /\  B  C_  x )  ->  ( A. y  e.  x  ( B  e.  On  ->  ( B  C_  y  ->  ch )
)  ->  ph ) )
6968exp31 590 . . . . 5  |-  ( Lim  x  ->  ( B  e.  On  ->  ( B  C_  x  ->  ( A. y  e.  x  ( B  e.  On  ->  ( B  C_  y  ->  ch ) )  ->  ph )
) ) )
7069com3l 77 . . . 4  |-  ( B  e.  On  ->  ( B  C_  x  ->  ( Lim  x  ->  ( A. y  e.  x  ( B  e.  On  ->  ( B  C_  y  ->  ch ) )  ->  ph )
) ) )
7170com4t 81 . . 3  |-  ( Lim  x  ->  ( A. y  e.  x  ( B  e.  On  ->  ( B  C_  y  ->  ch ) )  ->  ( B  e.  On  ->  ( B  C_  x  ->  ph ) ) ) )
7215, 19, 23, 27, 29, 63, 71tfinds 4622 . 2  |-  ( A  e.  On  ->  ( B  e.  On  ->  ( B  C_  A  ->  ta ) ) )
7372imp31 423 1  |-  ( ( ( A  e.  On  /\  B  e.  On )  /\  B  C_  A
)  ->  ta )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    /\ wa 360   E.wex 1537    = wceq 1619    e. wcel 1621    =/= wne 2421   A.wral 2518    C_ wss 3127   (/)c0 3430   Oncon0 4364   Lim wlim 4365   suc csuc 4366
This theorem is referenced by:  tfindsg2  4624  oaordi  6512  infensuc  7007  r1ordg  7418
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pr 4186  ax-un 4484
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-rab 2527  df-v 2765  df-sbc 2967  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-pss 3143  df-nul 3431  df-if 3540  df-pw 3601  df-sn 3620  df-pr 3621  df-tp 3622  df-op 3623  df-uni 3802  df-br 3998  df-opab 4052  df-tr 4088  df-eprel 4277  df-po 4286  df-so 4287  df-fr 4324  df-we 4326  df-ord 4367  df-on 4368  df-lim 4369  df-suc 4370
  Copyright terms: Public domain W3C validator