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 )