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

Theorem findsg 6731
Description: Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction step. The basis of this version is an arbitrary natural number  B instead of zero. (Contributed by NM, 16-Sep-1995.)
Hypotheses
Ref Expression
findsg.1  |-  ( x  =  B  ->  ( ph 
<->  ps ) )
findsg.2  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
findsg.3  |-  ( x  =  suc  y  -> 
( ph  <->  th ) )
findsg.4  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
findsg.5  |-  ( B  e.  om  ->  ps )
findsg.6  |-  ( ( ( y  e.  om  /\  B  e.  om )  /\  B  C_  y )  ->  ( ch  ->  th ) )
Assertion
Ref Expression
findsg  |-  ( ( ( A  e.  om  /\  B  e.  om )  /\  B  C_  A )  ->  ta )
Distinct variable groups:    x, A    x, y, B    ps, x    ch, x    th, x    ta, x    ph, y
Allowed substitution hints:    ph( x)    ps( y)    ch( y)    th( y)    ta( y)    A( y)

Proof of Theorem findsg
StepHypRef Expression
1 sseq2 3486 . . . . . . 7  |-  ( x  =  (/)  ->  ( B 
C_  x  <->  B  C_  (/) ) )
21adantl 467 . . . . . 6  |-  ( ( B  =  (/)  /\  x  =  (/) )  ->  ( B  C_  x  <->  B  C_  (/) ) )
3 eqeq2 2437 . . . . . . . 8  |-  ( B  =  (/)  ->  ( x  =  B  <->  x  =  (/) ) )
4 findsg.1 . . . . . . . 8  |-  ( x  =  B  ->  ( ph 
<->  ps ) )
53, 4syl6bir 232 . . . . . . 7  |-  ( B  =  (/)  ->  ( x  =  (/)  ->  ( ph  <->  ps ) ) )
65imp 430 . . . . . 6  |-  ( ( B  =  (/)  /\  x  =  (/) )  ->  ( ph 
<->  ps ) )
72, 6imbi12d 321 . . . . 5  |-  ( ( B  =  (/)  /\  x  =  (/) )  ->  (
( B  C_  x  ->  ph )  <->  ( B  C_  (/)  ->  ps ) ) )
81imbi1d 318 . . . . . 6  |-  ( x  =  (/)  ->  ( ( B  C_  x  ->  ph )  <->  ( B  C_  (/) 
->  ph ) ) )
9 ss0 3793 . . . . . . . . 9  |-  ( B 
C_  (/)  ->  B  =  (/) )
109con3i 140 . . . . . . . 8  |-  ( -.  B  =  (/)  ->  -.  B  C_  (/) )
1110pm2.21d 109 . . . . . . 7  |-  ( -.  B  =  (/)  ->  ( B  C_  (/)  ->  ( ph  <->  ps ) ) )
1211pm5.74d 250 . . . . . 6  |-  ( -.  B  =  (/)  ->  (
( B  C_  (/)  ->  ph )  <->  ( B  C_  (/)  ->  ps ) ) )
138, 12sylan9bbr 705 . . . . 5  |-  ( ( -.  B  =  (/)  /\  x  =  (/) )  -> 
( ( B  C_  x  ->  ph )  <->  ( B  C_  (/)  ->  ps ) ) )
147, 13pm2.61ian 797 . . . 4  |-  ( x  =  (/)  ->  ( ( B  C_  x  ->  ph )  <->  ( B  C_  (/) 
->  ps ) ) )
1514imbi2d 317 . . 3  |-  ( x  =  (/)  ->  ( ( B  e.  om  ->  ( B  C_  x  ->  ph ) )  <->  ( B  e.  om  ->  ( B  C_  (/)  ->  ps ) ) ) )
16 sseq2 3486 . . . . 5  |-  ( x  =  y  ->  ( B  C_  x  <->  B  C_  y
) )
17 findsg.2 . . . . 5  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
1816, 17imbi12d 321 . . . 4  |-  ( x  =  y  ->  (
( B  C_  x  ->  ph )  <->  ( B  C_  y  ->  ch )
) )
1918imbi2d 317 . . 3  |-  ( x  =  y  ->  (
( B  e.  om  ->  ( B  C_  x  ->  ph ) )  <->  ( B  e.  om  ->  ( B  C_  y  ->  ch )
) ) )
20 sseq2 3486 . . . . 5  |-  ( x  =  suc  y  -> 
( B  C_  x  <->  B 
C_  suc  y )
)
21 findsg.3 . . . . 5  |-  ( x  =  suc  y  -> 
( ph  <->  th ) )
2220, 21imbi12d 321 . . . 4  |-  ( x  =  suc  y  -> 
( ( B  C_  x  ->  ph )  <->  ( B  C_ 
suc  y  ->  th )
) )
2322imbi2d 317 . . 3  |-  ( x  =  suc  y  -> 
( ( B  e. 
om  ->  ( B  C_  x  ->  ph ) )  <->  ( B  e.  om  ->  ( B  C_ 
suc  y  ->  th )
) ) )
24 sseq2 3486 . . . . 5  |-  ( x  =  A  ->  ( B  C_  x  <->  B  C_  A
) )
25 findsg.4 . . . . 5  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
2624, 25imbi12d 321 . . . 4  |-  ( x  =  A  ->  (
( B  C_  x  ->  ph )  <->  ( B  C_  A  ->  ta )
) )
2726imbi2d 317 . . 3  |-  ( x  =  A  ->  (
( B  e.  om  ->  ( B  C_  x  ->  ph ) )  <->  ( B  e.  om  ->  ( B  C_  A  ->  ta )
) ) )
28 findsg.5 . . . 4  |-  ( B  e.  om  ->  ps )
2928a1d 26 . . 3  |-  ( B  e.  om  ->  ( B  C_  (/)  ->  ps )
)
30 vex 3084 . . . . . . . . . . . . . 14  |-  y  e. 
_V
3130sucex 6649 . . . . . . . . . . . . 13  |-  suc  y  e.  _V
3231eqvinc 3198 . . . . . . . . . . . 12  |-  ( suc  y  =  B  <->  E. x
( x  =  suc  y  /\  x  =  B ) )
3328, 4syl5ibr 224 . . . . . . . . . . . . . 14  |-  ( x  =  B  ->  ( B  e.  om  ->  ph ) )
3421biimpd 210 . . . . . . . . . . . . . 14  |-  ( x  =  suc  y  -> 
( ph  ->  th )
)
3533, 34sylan9r 662 . . . . . . . . . . . . 13  |-  ( ( x  =  suc  y  /\  x  =  B
)  ->  ( B  e.  om  ->  th )
)
3635exlimiv 1766 . . . . . . . . . . . 12  |-  ( E. x ( x  =  suc  y  /\  x  =  B )  ->  ( B  e.  om  ->  th ) )
3732, 36sylbi 198 . . . . . . . . . . 11  |-  ( suc  y  =  B  -> 
( B  e.  om  ->  th ) )
3837eqcoms 2434 . . . . . . . . . 10  |-  ( B  =  suc  y  -> 
( B  e.  om  ->  th ) )
3938imim2i 16 . . . . . . . . 9  |-  ( ( B  C_  suc  y  ->  B  =  suc  y )  ->  ( B  C_  suc  y  ->  ( B  e.  om  ->  th )
) )
4039a1d 26 . . . . . . . 8  |-  ( ( B  C_  suc  y  ->  B  =  suc  y )  ->  ( ( B 
C_  y  ->  ch )  ->  ( B  C_  suc  y  ->  ( B  e.  om  ->  th )
) ) )
4140com4r 89 . . . . . . 7  |-  ( B  e.  om  ->  (
( B  C_  suc  y  ->  B  =  suc  y )  ->  (
( B  C_  y  ->  ch )  ->  ( B  C_  suc  y  ->  th ) ) ) )
4241adantl 467 . . . . . 6  |-  ( ( y  e.  om  /\  B  e.  om )  ->  ( ( B  C_  suc  y  ->  B  =  suc  y )  -> 
( ( B  C_  y  ->  ch )  -> 
( B  C_  suc  y  ->  th ) ) ) )
43 df-ne 2620 . . . . . . . . 9  |-  ( B  =/=  suc  y  <->  -.  B  =  suc  y )
4443anbi2i 698 . . . . . . . 8  |-  ( ( B  C_  suc  y  /\  B  =/=  suc  y )  <->  ( B  C_  suc  y  /\  -.  B  =  suc  y ) )
45 annim 426 . . . . . . . 8  |-  ( ( B  C_  suc  y  /\  -.  B  =  suc  y )  <->  -.  ( B  C_  suc  y  ->  B  =  suc  y ) )
4644, 45bitri 252 . . . . . . 7  |-  ( ( B  C_  suc  y  /\  B  =/=  suc  y )  <->  -.  ( B  C_  suc  y  ->  B  =  suc  y ) )
47 nnon 6709 . . . . . . . . 9  |-  ( B  e.  om  ->  B  e.  On )
48 nnon 6709 . . . . . . . . 9  |-  ( y  e.  om  ->  y  e.  On )
49 onsssuc 5526 . . . . . . . . . 10  |-  ( ( B  e.  On  /\  y  e.  On )  ->  ( B  C_  y  <->  B  e.  suc  y ) )
50 suceloni 6651 . . . . . . . . . . 11  |-  ( y  e.  On  ->  suc  y  e.  On )
51 onelpss 5479 . . . . . . . . . . 11  |-  ( ( B  e.  On  /\  suc  y  e.  On )  ->  ( B  e. 
suc  y  <->  ( B  C_ 
suc  y  /\  B  =/=  suc  y ) ) )
5250, 51sylan2 476 . . . . . . . . . 10  |-  ( ( B  e.  On  /\  y  e.  On )  ->  ( B  e.  suc  y 
<->  ( B  C_  suc  y  /\  B  =/=  suc  y ) ) )
5349, 52bitrd 256 . . . . . . . . 9  |-  ( ( B  e.  On  /\  y  e.  On )  ->  ( B  C_  y  <->  ( B  C_  suc  y  /\  B  =/=  suc  y )
) )
5447, 48, 53syl2anr 480 . . . . . . . 8  |-  ( ( y  e.  om  /\  B  e.  om )  ->  ( B  C_  y  <->  ( B  C_  suc  y  /\  B  =/=  suc  y )
) )
55 findsg.6 . . . . . . . . . . . 12  |-  ( ( ( y  e.  om  /\  B  e.  om )  /\  B  C_  y )  ->  ( ch  ->  th ) )
5655ex 435 . . . . . . . . . . 11  |-  ( ( y  e.  om  /\  B  e.  om )  ->  ( B  C_  y  ->  ( ch  ->  th )
) )
57 ax-1 6 . . . . . . . . . . 11  |-  ( th 
->  ( B  C_  suc  y  ->  th ) )
5856, 57syl8 72 . . . . . . . . . 10  |-  ( ( y  e.  om  /\  B  e.  om )  ->  ( B  C_  y  ->  ( ch  ->  ( B  C_  suc  y  ->  th ) ) ) )
5958a2d 29 . . . . . . . . 9  |-  ( ( y  e.  om  /\  B  e.  om )  ->  ( ( B  C_  y  ->  ch )  -> 
( B  C_  y  ->  ( B  C_  suc  y  ->  th ) ) ) )
6059com23 81 . . . . . . . 8  |-  ( ( y  e.  om  /\  B  e.  om )  ->  ( B  C_  y  ->  ( ( B  C_  y  ->  ch )  -> 
( B  C_  suc  y  ->  th ) ) ) )
6154, 60sylbird 238 . . . . . . 7  |-  ( ( y  e.  om  /\  B  e.  om )  ->  ( ( B  C_  suc  y  /\  B  =/= 
suc  y )  -> 
( ( B  C_  y  ->  ch )  -> 
( B  C_  suc  y  ->  th ) ) ) )
6246, 61syl5bir 221 . . . . . 6  |-  ( ( y  e.  om  /\  B  e.  om )  ->  ( -.  ( B 
C_  suc  y  ->  B  =  suc  y )  ->  ( ( B 
C_  y  ->  ch )  ->  ( B  C_  suc  y  ->  th )
) ) )
6342, 62pm2.61d 161 . . . . 5  |-  ( ( y  e.  om  /\  B  e.  om )  ->  ( ( B  C_  y  ->  ch )  -> 
( B  C_  suc  y  ->  th ) ) )
6463ex 435 . . . 4  |-  ( y  e.  om  ->  ( B  e.  om  ->  ( ( B  C_  y  ->  ch )  ->  ( B  C_  suc  y  ->  th ) ) ) )
6564a2d 29 . . 3  |-  ( y  e.  om  ->  (
( B  e.  om  ->  ( B  C_  y  ->  ch ) )  -> 
( B  e.  om  ->  ( B  C_  suc  y  ->  th ) ) ) )
6615, 19, 23, 27, 29, 65finds 6730 . 2  |-  ( A  e.  om  ->  ( B  e.  om  ->  ( B  C_  A  ->  ta ) ) )
6766imp31 433 1  |-  ( ( ( A  e.  om  /\  B  e.  om )  /\  B  C_  A )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437   E.wex 1659    e. wcel 1868    =/= wne 2618    C_ wss 3436   (/)c0 3761   Oncon0 5439   suc csuc 5441   omcom 6703
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657  ax-un 6594
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-tr 4516  df-eprel 4761  df-po 4771  df-so 4772  df-fr 4809  df-we 4811  df-ord 5442  df-on 5443  df-lim 5444  df-suc 5445  df-om 6704
This theorem is referenced by:  nnaordi  7324  inf3lem5  8140  ackbij2lem4  8673  sornom  8708  fin23lem15  8765  fin23lem36  8779  isf32lem1  8784  isf32lem2  8785  wunex2  9164  indpi  9333
  Copyright terms: Public domain W3C validator