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

Theorem tfindes 6472
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 3187 . 2  |-  ( y  =  (/)  ->  ( [. y  /  x ]. ph  <->  [. (/)  /  x ]. ph ) )
2 dfsbcq 3187 . 2  |-  ( y  =  z  ->  ( [. y  /  x ]. ph  <->  [. z  /  x ]. ph ) )
3 dfsbcq 3187 . 2  |-  ( y  =  suc  z  -> 
( [. y  /  x ]. ph  <->  [. suc  z  /  x ]. ph ) )
4 sbceq2a 3197 . 2  |-  ( y  =  x  ->  ( [. y  /  x ]. ph  <->  ph ) )
5 tfindes.1 . 2  |-  [. (/)  /  x ]. ph
6 nfv 1673 . . . 4  |-  F/ x  z  e.  On
7 nfsbc1v 3205 . . . . 5  |-  F/ x [. z  /  x ]. ph
8 nfsbc1v 3205 . . . . 5  |-  F/ x [. suc  z  /  x ]. ph
97, 8nfim 1853 . . . 4  |-  F/ x
( [. z  /  x ]. ph  ->  [. suc  z  /  x ]. ph )
106, 9nfim 1853 . . 3  |-  F/ x
( z  e.  On  ->  ( [. z  /  x ]. ph  ->  [. suc  z  /  x ]. ph )
)
11 eleq1 2502 . . . 4  |-  ( x  =  z  ->  (
x  e.  On  <->  z  e.  On ) )
12 sbceq1a 3196 . . . . 5  |-  ( x  =  z  ->  ( ph 
<-> 
[. z  /  x ]. ph ) )
13 suceq 4783 . . . . . 6  |-  ( x  =  z  ->  suc  x  =  suc  z )
14 dfsbcq 3187 . . . . . 6  |-  ( suc  x  =  suc  z  ->  ( [. suc  x  /  x ]. ph  <->  [. suc  z  /  x ]. ph )
)
1513, 14syl 16 . . . . 5  |-  ( x  =  z  ->  ( [. suc  x  /  x ]. ph  <->  [. suc  z  /  x ]. ph ) )
1612, 15imbi12d 320 . . . 4  |-  ( x  =  z  ->  (
( ph  ->  [. suc  x  /  x ]. ph )  <->  (
[. z  /  x ]. ph  ->  [. suc  z  /  x ]. ph )
) )
1711, 16imbi12d 320 . . 3  |-  ( x  =  z  ->  (
( x  e.  On  ->  ( ph  ->  [. suc  x  /  x ]. ph )
)  <->  ( z  e.  On  ->  ( [. z  /  x ]. ph  ->  [.
suc  z  /  x ]. ph ) ) ) )
18 tfindes.2 . . 3  |-  ( x  e.  On  ->  ( ph  ->  [. suc  x  /  x ]. ph ) )
1910, 17, 18chvar 1957 . 2  |-  ( z  e.  On  ->  ( [. z  /  x ]. ph  ->  [. suc  z  /  x ]. ph )
)
20 cbvralsv 2957 . . . 4  |-  ( A. x  e.  y  ph  <->  A. z  e.  y  [
z  /  x ] ph )
21 sbsbc 3189 . . . . 5  |-  ( [ z  /  x ] ph 
<-> 
[. z  /  x ]. ph )
2221ralbii 2738 . . . 4  |-  ( A. z  e.  y  [
z  /  x ] ph 
<-> 
A. z  e.  y 
[. z  /  x ]. ph )
2320, 22bitri 249 . . 3  |-  ( A. x  e.  y  ph  <->  A. z  e.  y  [. z  /  x ]. ph )
24 tfindes.3 . . 3  |-  ( Lim  y  ->  ( A. x  e.  y  ph  ->  [. y  /  x ]. ph ) )
2523, 24syl5bir 218 . 2  |-  ( Lim  y  ->  ( A. z  e.  y  [. z  /  x ]. ph  ->  [. y  /  x ]. ph ) )
261, 2, 3, 4, 5, 19, 25tfinds 6469 1  |-  ( x  e.  On  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369   [wsb 1700    e. wcel 1756   A.wral 2714   [.wsbc 3185   (/)c0 3636   Oncon0 4718   Lim wlim 4719   suc csuc 4720
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 2423  ax-sep 4412  ax-nul 4420  ax-pr 4530  ax-un 6371
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 2257  df-mo 2258  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2719  df-rex 2720  df-rab 2723  df-v 2973  df-sbc 3186  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-pss 3343  df-nul 3637  df-if 3791  df-pw 3861  df-sn 3877  df-pr 3879  df-tp 3881  df-op 3883  df-uni 4091  df-br 4292  df-opab 4350  df-tr 4385  df-eprel 4631  df-po 4640  df-so 4641  df-fr 4678  df-we 4680  df-ord 4721  df-on 4722  df-lim 4723  df-suc 4724
This theorem is referenced by:  tfinds2  6473
  Copyright terms: Public domain W3C validator