Metamath Proof Explorer

Theorem tfindes

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)

Ref Expression
Hypotheses 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 tfindes 
|- ( x e. On -> ph )

Proof

Step Hyp Ref Expression
1 tfindes.1 
 |-  [. (/) / x ]. ph
2 tfindes.2 
 |-  ( x e. On -> ( ph -> [. suc x / x ]. ph ) )
3 tfindes.3 
 |-  ( Lim y -> ( A. x e. y ph -> [. y / x ]. ph ) )
4 dfsbcq 
 |-  ( y = (/) -> ( [. y / x ]. ph <-> [. (/) / x ]. ph ) )
5 dfsbcq 
 |-  ( y = z -> ( [. y / x ]. ph <-> [. z / x ]. ph ) )
6 dfsbcq 
 |-  ( y = suc z -> ( [. y / x ]. ph <-> [. suc z / x ]. ph ) )
7 sbceq2a 
 |-  ( y = x -> ( [. y / x ]. ph <-> ph ) )
8 nfv 
 |-  F/ x z e. On
9 nfsbc1v 
 |-  F/ x [. z / x ]. ph
10 nfsbc1v 
 |-  F/ x [. suc z / x ]. ph
11 9 10 nfim 
 |-  F/ x ( [. z / x ]. ph -> [. suc z / x ]. ph )
12 8 11 nfim 
 |-  F/ x ( z e. On -> ( [. z / x ]. ph -> [. suc z / x ]. ph ) )
13 eleq1w 
 |-  ( x = z -> ( x e. On <-> z e. On ) )
14 sbceq1a 
 |-  ( x = z -> ( ph <-> [. z / x ]. ph ) )
15 suceq 
 |-  ( x = z -> suc x = suc z )
16 15 sbceq1d 
 |-  ( x = z -> ( [. suc x / x ]. ph <-> [. suc z / x ]. ph ) )
17 14 16 imbi12d 
 |-  ( x = z -> ( ( ph -> [. suc x / x ]. ph ) <-> ( [. z / x ]. ph -> [. suc z / x ]. ph ) ) )
18 13 17 imbi12d 
 |-  ( x = z -> ( ( x e. On -> ( ph -> [. suc x / x ]. ph ) ) <-> ( z e. On -> ( [. z / x ]. ph -> [. suc z / x ]. ph ) ) ) )
19 12 18 2 chvarfv 
 |-  ( z e. On -> ( [. z / x ]. ph -> [. suc z / x ]. ph ) )
20 cbvralsvw 
 |-  ( A. x e. y ph <-> A. z e. y [ z / x ] ph )
21 sbsbc 
 |-  ( [ z / x ] ph <-> [. z / x ]. ph )
22 21 ralbii 
 |-  ( A. z e. y [ z / x ] ph <-> A. z e. y [. z / x ]. ph )
23 20 22 bitri 
 |-  ( A. x e. y ph <-> A. z e. y [. z / x ]. ph )
24 23 3 syl5bir 
 |-  ( Lim y -> ( A. z e. y [. z / x ]. ph -> [. y / x ]. ph ) )
25 4 5 6 7 1 19 24 tfinds 
 |-  ( x e. On -> ph )