Metamath Proof Explorer

Theorem findsg

Description: Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction step. The basis of this version is an arbitrary natural number B instead of zero. (Contributed by NM, 16-Sep-1995)

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

Proof

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