Metamath Proof Explorer


Theorem tfindsg

Description: Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. The basis of this version is an arbitrary ordinal B instead of zero. Remark in TakeutiZaring p. 57. (Contributed by NM, 5-Mar-2004)

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

Proof

Step Hyp Ref Expression
1 tfindsg.1
 |-  ( x = B -> ( ph <-> ps ) )
2 tfindsg.2
 |-  ( x = y -> ( ph <-> ch ) )
3 tfindsg.3
 |-  ( x = suc y -> ( ph <-> th ) )
4 tfindsg.4
 |-  ( x = A -> ( ph <-> ta ) )
5 tfindsg.5
 |-  ( B e. On -> ps )
6 tfindsg.6
 |-  ( ( ( y e. On /\ B e. On ) /\ B C_ y ) -> ( ch -> th ) )
7 tfindsg.7
 |-  ( ( ( Lim x /\ B e. On ) /\ B C_ x ) -> ( A. y e. x ( B C_ y -> ch ) -> ph ) )
8 sseq2
 |-  ( x = (/) -> ( B C_ x <-> B C_ (/) ) )
9 8 adantl
 |-  ( ( B = (/) /\ x = (/) ) -> ( B C_ x <-> B C_ (/) ) )
10 eqeq2
 |-  ( B = (/) -> ( x = B <-> x = (/) ) )
11 10 1 syl6bir
 |-  ( B = (/) -> ( x = (/) -> ( ph <-> ps ) ) )
12 11 imp
 |-  ( ( B = (/) /\ x = (/) ) -> ( ph <-> ps ) )
13 9 12 imbi12d
 |-  ( ( B = (/) /\ x = (/) ) -> ( ( B C_ x -> ph ) <-> ( B C_ (/) -> ps ) ) )
14 8 imbi1d
 |-  ( x = (/) -> ( ( B C_ x -> ph ) <-> ( B C_ (/) -> ph ) ) )
15 ss0
 |-  ( B C_ (/) -> B = (/) )
16 15 con3i
 |-  ( -. B = (/) -> -. B C_ (/) )
17 16 pm2.21d
 |-  ( -. B = (/) -> ( B C_ (/) -> ( ph <-> ps ) ) )
18 17 pm5.74d
 |-  ( -. B = (/) -> ( ( B C_ (/) -> ph ) <-> ( B C_ (/) -> ps ) ) )
19 14 18 sylan9bbr
 |-  ( ( -. B = (/) /\ x = (/) ) -> ( ( B C_ x -> ph ) <-> ( B C_ (/) -> ps ) ) )
20 13 19 pm2.61ian
 |-  ( x = (/) -> ( ( B C_ x -> ph ) <-> ( B C_ (/) -> ps ) ) )
21 20 imbi2d
 |-  ( x = (/) -> ( ( B e. On -> ( B C_ x -> ph ) ) <-> ( B e. On -> ( B C_ (/) -> ps ) ) ) )
22 sseq2
 |-  ( x = y -> ( B C_ x <-> B C_ y ) )
23 22 2 imbi12d
 |-  ( x = y -> ( ( B C_ x -> ph ) <-> ( B C_ y -> ch ) ) )
24 23 imbi2d
 |-  ( x = y -> ( ( B e. On -> ( B C_ x -> ph ) ) <-> ( B e. On -> ( B C_ y -> ch ) ) ) )
25 sseq2
 |-  ( x = suc y -> ( B C_ x <-> B C_ suc y ) )
26 25 3 imbi12d
 |-  ( x = suc y -> ( ( B C_ x -> ph ) <-> ( B C_ suc y -> th ) ) )
27 26 imbi2d
 |-  ( x = suc y -> ( ( B e. On -> ( B C_ x -> ph ) ) <-> ( B e. On -> ( B C_ suc y -> th ) ) ) )
28 sseq2
 |-  ( x = A -> ( B C_ x <-> B C_ A ) )
29 28 4 imbi12d
 |-  ( x = A -> ( ( B C_ x -> ph ) <-> ( B C_ A -> ta ) ) )
30 29 imbi2d
 |-  ( x = A -> ( ( B e. On -> ( B C_ x -> ph ) ) <-> ( B e. On -> ( B C_ A -> ta ) ) ) )
31 5 a1d
 |-  ( B e. On -> ( B C_ (/) -> ps ) )
32 vex
 |-  y e. _V
33 32 sucex
 |-  suc y e. _V
34 33 eqvinc
 |-  ( suc y = B <-> E. x ( x = suc y /\ x = B ) )
35 5 1 syl5ibr
 |-  ( x = B -> ( B e. On -> ph ) )
36 3 biimpd
 |-  ( x = suc y -> ( ph -> th ) )
37 35 36 sylan9r
 |-  ( ( x = suc y /\ x = B ) -> ( B e. On -> th ) )
38 37 exlimiv
 |-  ( E. x ( x = suc y /\ x = B ) -> ( B e. On -> th ) )
39 34 38 sylbi
 |-  ( suc y = B -> ( B e. On -> th ) )
40 39 eqcoms
 |-  ( B = suc y -> ( B e. On -> th ) )
41 40 imim2i
 |-  ( ( B C_ suc y -> B = suc y ) -> ( B C_ suc y -> ( B e. On -> th ) ) )
42 41 a1d
 |-  ( ( B C_ suc y -> B = suc y ) -> ( ( B C_ y -> ch ) -> ( B C_ suc y -> ( B e. On -> th ) ) ) )
43 42 com4r
 |-  ( B e. On -> ( ( B C_ suc y -> B = suc y ) -> ( ( B C_ y -> ch ) -> ( B C_ suc y -> th ) ) ) )
44 43 adantl
 |-  ( ( y e. On /\ B e. On ) -> ( ( B C_ suc y -> B = suc y ) -> ( ( B C_ y -> ch ) -> ( B C_ suc y -> th ) ) ) )
45 df-ne
 |-  ( B =/= suc y <-> -. B = suc y )
46 45 anbi2i
 |-  ( ( B C_ suc y /\ B =/= suc y ) <-> ( B C_ suc y /\ -. B = suc y ) )
47 annim
 |-  ( ( B C_ suc y /\ -. B = suc y ) <-> -. ( B C_ suc y -> B = suc y ) )
48 46 47 bitri
 |-  ( ( B C_ suc y /\ B =/= suc y ) <-> -. ( B C_ suc y -> B = suc y ) )
49 onsssuc
 |-  ( ( B e. On /\ y e. On ) -> ( B C_ y <-> B e. suc y ) )
50 suceloni
 |-  ( y e. On -> suc y e. On )
51 onelpss
 |-  ( ( B e. On /\ suc y e. On ) -> ( B e. suc y <-> ( B C_ suc y /\ B =/= suc y ) ) )
52 50 51 sylan2
 |-  ( ( B e. On /\ y e. On ) -> ( B e. suc y <-> ( B C_ suc y /\ B =/= suc y ) ) )
53 49 52 bitrd
 |-  ( ( B e. On /\ y e. On ) -> ( B C_ y <-> ( B C_ suc y /\ B =/= suc y ) ) )
54 53 ancoms
 |-  ( ( y e. On /\ B e. On ) -> ( B C_ y <-> ( B C_ suc y /\ B =/= suc y ) ) )
55 6 ex
 |-  ( ( y e. On /\ B e. On ) -> ( B C_ y -> ( ch -> th ) ) )
56 55 a1ddd
 |-  ( ( y e. On /\ B e. On ) -> ( B C_ y -> ( ch -> ( B C_ suc y -> th ) ) ) )
57 56 a2d
 |-  ( ( y e. On /\ B e. On ) -> ( ( B C_ y -> ch ) -> ( B C_ y -> ( B C_ suc y -> th ) ) ) )
58 57 com23
 |-  ( ( y e. On /\ B e. On ) -> ( B C_ y -> ( ( B C_ y -> ch ) -> ( B C_ suc y -> th ) ) ) )
59 54 58 sylbird
 |-  ( ( y e. On /\ B e. On ) -> ( ( B C_ suc y /\ B =/= suc y ) -> ( ( B C_ y -> ch ) -> ( B C_ suc y -> th ) ) ) )
60 48 59 syl5bir
 |-  ( ( y e. On /\ B e. On ) -> ( -. ( B C_ suc y -> B = suc y ) -> ( ( B C_ y -> ch ) -> ( B C_ suc y -> th ) ) ) )
61 44 60 pm2.61d
 |-  ( ( y e. On /\ B e. On ) -> ( ( B C_ y -> ch ) -> ( B C_ suc y -> th ) ) )
62 61 ex
 |-  ( y e. On -> ( B e. On -> ( ( B C_ y -> ch ) -> ( B C_ suc y -> th ) ) ) )
63 62 a2d
 |-  ( y e. On -> ( ( B e. On -> ( B C_ y -> ch ) ) -> ( B e. On -> ( B C_ suc y -> th ) ) ) )
64 pm2.27
 |-  ( B e. On -> ( ( B e. On -> ( B C_ y -> ch ) ) -> ( B C_ y -> ch ) ) )
65 64 ralimdv
 |-  ( B e. On -> ( A. y e. x ( B e. On -> ( B C_ y -> ch ) ) -> A. y e. x ( B C_ y -> ch ) ) )
66 65 ad2antlr
 |-  ( ( ( Lim x /\ B e. On ) /\ B C_ x ) -> ( A. y e. x ( B e. On -> ( B C_ y -> ch ) ) -> A. y e. x ( B C_ y -> ch ) ) )
67 66 7 syld
 |-  ( ( ( Lim x /\ B e. On ) /\ B C_ x ) -> ( A. y e. x ( B e. On -> ( B C_ y -> ch ) ) -> ph ) )
68 67 exp31
 |-  ( Lim x -> ( B e. On -> ( B C_ x -> ( A. y e. x ( B e. On -> ( B C_ y -> ch ) ) -> ph ) ) ) )
69 68 com3l
 |-  ( B e. On -> ( B C_ x -> ( Lim x -> ( A. y e. x ( B e. On -> ( B C_ y -> ch ) ) -> ph ) ) ) )
70 69 com4t
 |-  ( Lim x -> ( A. y e. x ( B e. On -> ( B C_ y -> ch ) ) -> ( B e. On -> ( B C_ x -> ph ) ) ) )
71 21 24 27 30 31 63 70 tfinds
 |-  ( A e. On -> ( B e. On -> ( B C_ A -> ta ) ) )
72 71 imp31
 |-  ( ( ( A e. On /\ B e. On ) /\ B C_ A ) -> ta )