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

Theorem tfindes 6694
Description: Transfinite Induction with explicit substitution. The first hypothesis is the basis, the second is the induction step for successors, and the third is the induction step for limit ordinals. Theorem Schema 4 of [Suppes] p. 197. (Contributed by NM, 5-Mar-2004.)
Hypotheses
Ref Expression
tfindes.1  |-  [. (/)  /  x ]. ph
tfindes.2  |-  ( x  e.  On  ->  ( ph  ->  [. suc  x  /  x ]. ph ) )
tfindes.3  |-  ( Lim  y  ->  ( A. x  e.  y  ph  ->  [. y  /  x ]. ph ) )
Assertion
Ref Expression
tfindes  |-  ( x  e.  On  ->  ph )
Distinct variable groups:    x, y    ph, y
Allowed substitution hint:    ph( x)

Proof of Theorem tfindes
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 dfsbcq 3298 . 2  |-  ( y  =  (/)  ->  ( [. y  /  x ]. ph  <->  [. (/)  /  x ]. ph ) )
2 dfsbcq 3298 . 2  |-  ( y  =  z  ->  ( [. y  /  x ]. ph  <->  [. z  /  x ]. ph ) )
3 dfsbcq 3298 . 2  |-  ( y  =  suc  z  -> 
( [. y  /  x ]. ph  <->  [. suc  z  /  x ]. ph ) )
4 sbceq2a 3308 . 2  |-  ( y  =  x  ->  ( [. y  /  x ]. ph  <->  ph ) )
5 tfindes.1 . 2  |-  [. (/)  /  x ]. ph
6 nfv 1751 . . . 4  |-  F/ x  z  e.  On
7 nfsbc1v 3316 . . . . 5  |-  F/ x [. z  /  x ]. ph
8 nfsbc1v 3316 . . . . 5  |-  F/ x [. suc  z  /  x ]. ph
97, 8nfim 1975 . . . 4  |-  F/ x
( [. z  /  x ]. ph  ->  [. suc  z  /  x ]. ph )
106, 9nfim 1975 . . 3  |-  F/ x
( z  e.  On  ->  ( [. z  /  x ]. ph  ->  [. suc  z  /  x ]. ph )
)
11 eleq1 2492 . . . 4  |-  ( x  =  z  ->  (
x  e.  On  <->  z  e.  On ) )
12 sbceq1a 3307 . . . . 5  |-  ( x  =  z  ->  ( ph 
<-> 
[. z  /  x ]. ph ) )
13 suceq 5498 . . . . . 6  |-  ( x  =  z  ->  suc  x  =  suc  z )
1413sbceq1d 3301 . . . . 5  |-  ( x  =  z  ->  ( [. suc  x  /  x ]. ph  <->  [. suc  z  /  x ]. ph ) )
1512, 14imbi12d 321 . . . 4  |-  ( x  =  z  ->  (
( ph  ->  [. suc  x  /  x ]. ph )  <->  (
[. z  /  x ]. ph  ->  [. suc  z  /  x ]. ph )
) )
1611, 15imbi12d 321 . . 3  |-  ( x  =  z  ->  (
( x  e.  On  ->  ( ph  ->  [. suc  x  /  x ]. ph )
)  <->  ( z  e.  On  ->  ( [. z  /  x ]. ph  ->  [.
suc  z  /  x ]. ph ) ) ) )
17 tfindes.2 . . 3  |-  ( x  e.  On  ->  ( ph  ->  [. suc  x  /  x ]. ph ) )
1810, 16, 17chvar 2066 . 2  |-  ( z  e.  On  ->  ( [. z  /  x ]. ph  ->  [. suc  z  /  x ]. ph )
)
19 cbvralsv 3064 . . . 4  |-  ( A. x  e.  y  ph  <->  A. z  e.  y  [
z  /  x ] ph )
20 sbsbc 3300 . . . . 5  |-  ( [ z  /  x ] ph 
<-> 
[. z  /  x ]. ph )
2120ralbii 2854 . . . 4  |-  ( A. z  e.  y  [
z  /  x ] ph 
<-> 
A. z  e.  y 
[. z  /  x ]. ph )
2219, 21bitri 252 . . 3  |-  ( A. x  e.  y  ph  <->  A. z  e.  y  [. z  /  x ]. ph )
23 tfindes.3 . . 3  |-  ( Lim  y  ->  ( A. x  e.  y  ph  ->  [. y  /  x ]. ph ) )
2422, 23syl5bir 221 . 2  |-  ( Lim  y  ->  ( A. z  e.  y  [. z  /  x ]. ph  ->  [. y  /  x ]. ph ) )
251, 2, 3, 4, 5, 18, 24tfinds 6691 1  |-  ( x  e.  On  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   [wsb 1786    e. wcel 1867   A.wral 2773   [.wsbc 3296   (/)c0 3758   Oncon0 5433   Lim wlim 5434   suc csuc 5435
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 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pr 4652  ax-un 6588
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 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-sbc 3297  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-tr 4512  df-eprel 4756  df-po 4766  df-so 4767  df-fr 4804  df-we 4806  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439
This theorem is referenced by:  tfinds2  6695
  Copyright terms: Public domain W3C validator