Metamath Proof Explorer


Theorem tfis

Description: Transfinite Induction Schema. If all ordinal numbers less than a given number x have a property (induction hypothesis), then all ordinal numbers have the property (conclusion). Exercise 25 of Enderton p. 200. (Contributed by NM, 1-Aug-1994) (Revised by Mario Carneiro, 20-Nov-2016)

Ref Expression
Hypothesis tfis.1
|- ( x e. On -> ( A. y e. x [ y / x ] ph -> ph ) )
Assertion tfis
|- ( x e. On -> ph )

Proof

Step Hyp Ref Expression
1 tfis.1
 |-  ( x e. On -> ( A. y e. x [ y / x ] ph -> ph ) )
2 ssrab2
 |-  { x e. On | ph } C_ On
3 nfcv
 |-  F/_ x z
4 nfrab1
 |-  F/_ x { x e. On | ph }
5 3 4 nfss
 |-  F/ x z C_ { x e. On | ph }
6 4 nfcri
 |-  F/ x z e. { x e. On | ph }
7 5 6 nfim
 |-  F/ x ( z C_ { x e. On | ph } -> z e. { x e. On | ph } )
8 dfss3
 |-  ( x C_ { x e. On | ph } <-> A. y e. x y e. { x e. On | ph } )
9 sseq1
 |-  ( x = z -> ( x C_ { x e. On | ph } <-> z C_ { x e. On | ph } ) )
10 8 9 bitr3id
 |-  ( x = z -> ( A. y e. x y e. { x e. On | ph } <-> z C_ { x e. On | ph } ) )
11 rabid
 |-  ( x e. { x e. On | ph } <-> ( x e. On /\ ph ) )
12 eleq1w
 |-  ( x = z -> ( x e. { x e. On | ph } <-> z e. { x e. On | ph } ) )
13 11 12 bitr3id
 |-  ( x = z -> ( ( x e. On /\ ph ) <-> z e. { x e. On | ph } ) )
14 10 13 imbi12d
 |-  ( x = z -> ( ( A. y e. x y e. { x e. On | ph } -> ( x e. On /\ ph ) ) <-> ( z C_ { x e. On | ph } -> z e. { x e. On | ph } ) ) )
15 sbequ
 |-  ( w = y -> ( [ w / x ] ph <-> [ y / x ] ph ) )
16 nfcv
 |-  F/_ x On
17 nfcv
 |-  F/_ w On
18 nfv
 |-  F/ w ph
19 nfs1v
 |-  F/ x [ w / x ] ph
20 sbequ12
 |-  ( x = w -> ( ph <-> [ w / x ] ph ) )
21 16 17 18 19 20 cbvrabw
 |-  { x e. On | ph } = { w e. On | [ w / x ] ph }
22 15 21 elrab2
 |-  ( y e. { x e. On | ph } <-> ( y e. On /\ [ y / x ] ph ) )
23 22 simprbi
 |-  ( y e. { x e. On | ph } -> [ y / x ] ph )
24 23 ralimi
 |-  ( A. y e. x y e. { x e. On | ph } -> A. y e. x [ y / x ] ph )
25 24 1 syl5
 |-  ( x e. On -> ( A. y e. x y e. { x e. On | ph } -> ph ) )
26 25 anc2li
 |-  ( x e. On -> ( A. y e. x y e. { x e. On | ph } -> ( x e. On /\ ph ) ) )
27 3 7 14 26 vtoclgaf
 |-  ( z e. On -> ( z C_ { x e. On | ph } -> z e. { x e. On | ph } ) )
28 27 rgen
 |-  A. z e. On ( z C_ { x e. On | ph } -> z e. { x e. On | ph } )
29 tfi
 |-  ( ( { x e. On | ph } C_ On /\ A. z e. On ( z C_ { x e. On | ph } -> z e. { x e. On | ph } ) ) -> { x e. On | ph } = On )
30 2 28 29 mp2an
 |-  { x e. On | ph } = On
31 30 eqcomi
 |-  On = { x e. On | ph }
32 31 rabeq2i
 |-  ( x e. On <-> ( x e. On /\ ph ) )
33 32 simprbi
 |-  ( x e. On -> ph )