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 )