Metamath Proof Explorer

Theorem tfinds2

Description: Transfinite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last three are the basis and the induction hypotheses (for successor and limit ordinals respectively). Theorem Schema 4 of Suppes p. 197. The wff ta is an auxiliary antecedent to help shorten proofs using this theorem. (Contributed by NM, 4-Sep-2004)

Ref Expression
Hypotheses tfinds2.1 
|- ( x = (/) -> ( ph <-> ps ) )
tfinds2.2 
|- ( x = y -> ( ph <-> ch ) )
tfinds2.3 
|- ( x = suc y -> ( ph <-> th ) )
tfinds2.4 
|- ( ta -> ps )
tfinds2.5 
|- ( y e. On -> ( ta -> ( ch -> th ) ) )
tfinds2.6 
|- ( Lim x -> ( ta -> ( A. y e. x ch -> ph ) ) )
Assertion tfinds2 
|- ( x e. On -> ( ta -> ph ) )

Proof

Step Hyp Ref Expression
1 tfinds2.1 
 |-  ( x = (/) -> ( ph <-> ps ) )
2 tfinds2.2 
 |-  ( x = y -> ( ph <-> ch ) )
3 tfinds2.3 
 |-  ( x = suc y -> ( ph <-> th ) )
4 tfinds2.4 
 |-  ( ta -> ps )
5 tfinds2.5 
 |-  ( y e. On -> ( ta -> ( ch -> th ) ) )
6 tfinds2.6 
 |-  ( Lim x -> ( ta -> ( A. y e. x ch -> ph ) ) )
7 0ex 
 |-  (/) e. _V
8 1 imbi2d 
 |-  ( x = (/) -> ( ( ta -> ph ) <-> ( ta -> ps ) ) )
9 7 8 sbcie 
 |-  ( [. (/) / x ]. ( ta -> ph ) <-> ( ta -> ps ) )
10 4 9 mpbir 
 |-  [. (/) / x ]. ( ta -> ph )
11 5 a2d 
 |-  ( y e. On -> ( ( ta -> ch ) -> ( ta -> th ) ) )
12 11 sbcth 
 |-  ( x e. _V -> [. x / y ]. ( y e. On -> ( ( ta -> ch ) -> ( ta -> th ) ) ) )
13 12 elv 
 |-  [. x / y ]. ( y e. On -> ( ( ta -> ch ) -> ( ta -> th ) ) )
14 sbcimg 
 |-  ( x e. _V -> ( [. x / y ]. ( y e. On -> ( ( ta -> ch ) -> ( ta -> th ) ) ) <-> ( [. x / y ]. y e. On -> [. x / y ]. ( ( ta -> ch ) -> ( ta -> th ) ) ) ) )
15 14 elv 
 |-  ( [. x / y ]. ( y e. On -> ( ( ta -> ch ) -> ( ta -> th ) ) ) <-> ( [. x / y ]. y e. On -> [. x / y ]. ( ( ta -> ch ) -> ( ta -> th ) ) ) )
16 13 15 mpbi 
 |-  ( [. x / y ]. y e. On -> [. x / y ]. ( ( ta -> ch ) -> ( ta -> th ) ) )
17 sbcel1v 
 |-  ( [. x / y ]. y e. On <-> x e. On )
18 sbcimg 
 |-  ( x e. _V -> ( [. x / y ]. ( ( ta -> ch ) -> ( ta -> th ) ) <-> ( [. x / y ]. ( ta -> ch ) -> [. x / y ]. ( ta -> th ) ) ) )
19 18 elv 
 |-  ( [. x / y ]. ( ( ta -> ch ) -> ( ta -> th ) ) <-> ( [. x / y ]. ( ta -> ch ) -> [. x / y ]. ( ta -> th ) ) )
20 16 17 19 3imtr3i 
 |-  ( x e. On -> ( [. x / y ]. ( ta -> ch ) -> [. x / y ]. ( ta -> th ) ) )
21 vex 
 |-  x e. _V
22 2 bicomd 
 |-  ( x = y -> ( ch <-> ph ) )
23 22 equcoms 
 |-  ( y = x -> ( ch <-> ph ) )
24 23 imbi2d 
 |-  ( y = x -> ( ( ta -> ch ) <-> ( ta -> ph ) ) )
25 21 24 sbcie 
 |-  ( [. x / y ]. ( ta -> ch ) <-> ( ta -> ph ) )
26 vex 
 |-  y e. _V
27 26 sucex 
 |-  suc y e. _V
28 3 imbi2d 
 |-  ( x = suc y -> ( ( ta -> ph ) <-> ( ta -> th ) ) )
29 27 28 sbcie 
 |-  ( [. suc y / x ]. ( ta -> ph ) <-> ( ta -> th ) )
30 29 sbcbii 
 |-  ( [. x / y ]. [. suc y / x ]. ( ta -> ph ) <-> [. x / y ]. ( ta -> th ) )
31 suceq 
 |-  ( x = y -> suc x = suc y )
32 31 sbcco2 
 |-  ( [. x / y ]. [. suc y / x ]. ( ta -> ph ) <-> [. suc x / x ]. ( ta -> ph ) )
33 30 32 bitr3i 
 |-  ( [. x / y ]. ( ta -> th ) <-> [. suc x / x ]. ( ta -> ph ) )
34 20 25 33 3imtr3g 
 |-  ( x e. On -> ( ( ta -> ph ) -> [. suc x / x ]. ( ta -> ph ) ) )
35 2 imbi2d 
 |-  ( x = y -> ( ( ta -> ph ) <-> ( ta -> ch ) ) )
36 35 sbralie 
 |-  ( A. x e. y ( ta -> ph ) <-> [ y / x ] A. y e. x ( ta -> ch ) )
37 sbsbc 
 |-  ( [ y / x ] A. y e. x ( ta -> ch ) <-> [. y / x ]. A. y e. x ( ta -> ch ) )
38 36 37 bitr2i 
 |-  ( [. y / x ]. A. y e. x ( ta -> ch ) <-> A. x e. y ( ta -> ph ) )
39 r19.21v 
 |-  ( A. y e. x ( ta -> ch ) <-> ( ta -> A. y e. x ch ) )
40 6 a2d 
 |-  ( Lim x -> ( ( ta -> A. y e. x ch ) -> ( ta -> ph ) ) )
41 39 40 syl5bi 
 |-  ( Lim x -> ( A. y e. x ( ta -> ch ) -> ( ta -> ph ) ) )
42 41 sbcth 
 |-  ( y e. _V -> [. y / x ]. ( Lim x -> ( A. y e. x ( ta -> ch ) -> ( ta -> ph ) ) ) )
43 42 elv 
 |-  [. y / x ]. ( Lim x -> ( A. y e. x ( ta -> ch ) -> ( ta -> ph ) ) )
44 sbcimg 
 |-  ( y e. _V -> ( [. y / x ]. ( Lim x -> ( A. y e. x ( ta -> ch ) -> ( ta -> ph ) ) ) <-> ( [. y / x ]. Lim x -> [. y / x ]. ( A. y e. x ( ta -> ch ) -> ( ta -> ph ) ) ) ) )
45 44 elv 
 |-  ( [. y / x ]. ( Lim x -> ( A. y e. x ( ta -> ch ) -> ( ta -> ph ) ) ) <-> ( [. y / x ]. Lim x -> [. y / x ]. ( A. y e. x ( ta -> ch ) -> ( ta -> ph ) ) ) )
46 43 45 mpbi 
 |-  ( [. y / x ]. Lim x -> [. y / x ]. ( A. y e. x ( ta -> ch ) -> ( ta -> ph ) ) )
47 limeq 
 |-  ( x = y -> ( Lim x <-> Lim y ) )
48 26 47 sbcie 
 |-  ( [. y / x ]. Lim x <-> Lim y )
49 sbcimg 
 |-  ( y e. _V -> ( [. y / x ]. ( A. y e. x ( ta -> ch ) -> ( ta -> ph ) ) <-> ( [. y / x ]. A. y e. x ( ta -> ch ) -> [. y / x ]. ( ta -> ph ) ) ) )
50 49 elv 
 |-  ( [. y / x ]. ( A. y e. x ( ta -> ch ) -> ( ta -> ph ) ) <-> ( [. y / x ]. A. y e. x ( ta -> ch ) -> [. y / x ]. ( ta -> ph ) ) )
51 46 48 50 3imtr3i 
 |-  ( Lim y -> ( [. y / x ]. A. y e. x ( ta -> ch ) -> [. y / x ]. ( ta -> ph ) ) )
52 38 51 syl5bir 
 |-  ( Lim y -> ( A. x e. y ( ta -> ph ) -> [. y / x ]. ( ta -> ph ) ) )
53 10 34 52 tfindes 
 |-  ( x e. On -> ( ta -> ph ) )