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 ) )