Theorem findsg 3219

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 hypothesis. The basis of this version is an arbitrary natural number B instead of zero.

Hypotheses

Ref	Expression
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 (_ y) -> (ch -> th))

Assertion

Ref	Expression
findsg	|- (((A e. om /\ B e. om) /\ B (_ A) -> ta)

Distinct variable groups:   x,A   x,y,B   ps,x   ch,x   th,x   ta,x   ph,y

Proof of Theorem findsg

Step	Hyp	Ref	Expression
1		sseq2 2127	. . . . . . 7 |- (x = (/) -> (B (_ x <-> B (_ (/)))
2	1	adantl 388	. . . . . 6 |- ((B = (/) /\ x = (/)) -> (B (_ x <-> B (_ (/)))
3		eqeq2 1521	. . . . . . . 8 |- (B = (/) -> (x = B <-> x = (/)))
4		findsg.1	. . . . . . . 8 |- (x = B -> (ph <-> ps))
5	3, 4	syl6bir 213	. . . . . . 7 |- (B = (/) -> (x = (/) -> (ph <-> ps)))
6	5	imp 348	. . . . . 6 |- ((B = (/) /\ x = (/)) -> (ph <-> ps))
7	2, 6	imbi12d 628	. . . . 5 |- ((B = (/) /\ x = (/)) -> ((B (_ x -> ph) <-> (B (_ (/) -> ps)))
8	1	imbi1d 615	. . . . . 6 |- (x = (/) -> ((B (_ x -> ph) <-> (B (_ (/) -> ph)))
9		ss0 2348	. . . . . . . . 9 |- (B (_ (/) -> B = (/))
10	9	con3i 98	. . . . . . . 8 |- (-. B = (/) -> -. B (_ (/))
11	10	pm2.21d 78	. . . . . . 7 |- (-. B = (/) -> (B (_ (/) -> (ph <-> ps)))
12	11	pm5.74d 587	. . . . . 6 |- (-. B = (/) -> ((B (_ (/) -> ph) <-> (B (_ (/) -> ps)))
13	8, 12	sylan9bbr 543	. . . . 5 |- ((-. B = (/) /\ x = (/)) -> ((B (_ x -> ph) <-> (B (_ (/) -> ps)))
14	7, 13	pm2.61ian 478	. . . 4 |- (x = (/) -> ((B (_ x -> ph) <-> (B (_ (/) -> ps)))
15	14	imbi2d 614	. . 3 |- (x = (/) -> ((B e. om -> (B (_ x -> ph)) <-> (B e. om -> (B (_ (/) -> ps))))
16		sseq2 2127	. . . . 5 |- (x = y -> (B (_ x <-> B (_ y))
17		findsg.2	. . . . 5 |- (x = y -> (ph <-> ch))
18	16, 17	imbi12d 628	. . . 4 |- (x = y -> ((B (_ x -> ph) <-> (B (_ y -> ch)))
19	18	imbi2d 614	. . 3 |- (x = y -> ((B e. om -> (B (_ x -> ph)) <-> (B e. om -> (B (_ y -> ch))))
20		sseq2 2127	. . . . 5 |- (x = suc y -> (B (_ x <-> B (_ suc y))
21		findsg.3	. . . . 5 |- (x = suc y -> (ph <-> th))
22	20, 21	imbi12d 628	. . . 4 |- (x = suc y -> ((B (_ x -> ph) <-> (B (_ suc y -> th)))
23	22	imbi2d 614	. . 3 |- (x = suc y -> ((B e. om -> (B (_ x -> ph)) <-> (B e. om -> (B (_ suc y -> th))))
24		sseq2 2127	. . . . 5 |- (x = A -> (B (_ x <-> B (_ A))
25		findsg.4	. . . . 5 |- (x = A -> (ph <-> ta))
26	24, 25	imbi12d 628	. . . 4 |- (x = A -> ((B (_ x -> ph) <-> (B (_ A -> ta)))
27	26	imbi2d 614	. . 3 |- (x = A -> ((B e. om -> (B (_ x -> ph)) <-> (B e. om -> (B (_ A -> ta))))
28		findsg.5	. . . 4 |- (B e. om -> ps)
29	28	a1d 12	. . 3 |- (B e. om -> (B (_ (/) -> ps))
30		visset 1851	. . . . . . . . . . . . . 14 |- y e. V
31	30	sucex 3105	. . . . . . . . . . . . 13 |- suc y e. V
32	31	eqvinc 1921	. . . . . . . . . . . 12 |- (suc y = B <-> E.x(x = suc y /\ x = B))
33	4, 28	syl5bir 208	. . . . . . . . . . . . . 14 |- (x = B -> (B e. om -> ph))
34	21	biimpd 151	. . . . . . . . . . . . . 14 |- (x = suc y -> (ph -> th))
35	33, 34	sylan9r 471	. . . . . . . . . . . . 13 |- ((x = suc y /\ x = B) -> (B e. om -> th))
36	35	19.23aiv 1328	. . . . . . . . . . . 12 |- (E.x(x = suc y /\ x = B) -> (B e. om -> th))
37	32, 36	sylbi 197	. . . . . . . . . . 11 |- (suc y = B -> (B e. om -> th))
38	37	eqcoms 1515	. . . . . . . . . 10 |- (B = suc y -> (B e. om -> th))
39	38	imim2i 17	. . . . . . . . 9 |- ((B (_ suc y -> B = suc y) -> (B (_ suc y -> (B e. om -> th)))
40	39	a1d 12	. . . . . . . 8 |- ((B (_ suc y -> B = suc y) -> ((B (_ y -> ch) -> (B (_ suc y -> (B e. om -> th))))
41	40	com4r 41	. . . . . . 7 |- (B e. om -> ((B (_ suc y -> B = suc y) -> ((B (_ y -> ch) -> (B (_ suc y -> th))))
42	41	adantl 388	. . . . . 6 |- ((y e. om /\ B e. om) -> ((B (_ suc y -> B = suc y) -> ((B (_ y -> ch) -> (B (_ suc y -> th))))
43		onsssuc 3113	. . . . . . . . . . 11 |- ((B e. On /\ y e. On) -> (B (_ y <-> B e. suc y))
44		onelpss 3053	. . . . . . . . . . . 12 |- ((B e. On /\ suc y e. On) -> (B e. suc y <-> (B (_ suc y /\ B =/= suc y)))
45		suceloni 3117	. . . . . . . . . . . 12 |- (y e. On -> suc y e. On)
46	44, 45	sylan2 453	. . . . . . . . . . 11 |- ((B e. On /\ y e. On) -> (B e. suc y <-> (B (_ suc y /\ B =/= suc y)))
47	43, 46	bitrd 530	. . . . . . . . . 10 |- ((B e. On /\ y e. On) -> (B (_ y <-> (B (_ suc y /\ B =/= suc y)))
48		nnont 3199	. . . . . . . . . 10 |- (B e. om -> B e. On)
49		nnont 3199	. . . . . . . . . 10 |- (y e. om -> y e. On)
50	47, 48, 49	syl2an 456	. . . . . . . . 9 |- ((B e. om /\ y e. om) -> (B (_ y <-> (B (_ suc y /\ B =/= suc y)))
51	50	ancoms 438	. . . . . . . 8 |- ((y e. om /\ B e. om) -> (B (_ y <-> (B (_ suc y /\ B =/= suc y)))
52		findsg.6	. . . . . . . . . . . 12 |- (((y e. om /\ B e. om) /\ B (_ y) -> (ch -> th))
53	52	ex 371	. . . . . . . . . . 11 |- ((y e. om /\ B e. om) -> (B (_ y -> (ch -> th)))
54		ax-1 4	. . . . . . . . . . 11 |- (th -> (B (_ suc y -> th))
55	53, 54	syl8 24	. . . . . . . . . 10 |- ((y e. om /\ B e. om) -> (B (_ y -> (ch -> (B (_ suc y -> th))))
56	55	a2d 13	. . . . . . . . 9 |- ((y e. om /\ B e. om) -> ((B (_ y -> ch) -> (B (_ y -> (B (_ suc y -> th))))
57	56	com23 32	. . . . . . . 8 |- ((y e. om /\ B e. om) -> (B (_ y -> ((B (_ y -> ch) -> (B (_ suc y -> th))))
58	51, 57	sylbird 203	. . . . . . 7 |- ((y e. om /\ B e. om) -> ((B (_ suc y /\ B =/= suc y) -> ((B (_ y -> ch) -> (B (_ suc y -> th))))
59		df-ne 1624	. . . . . . . . 9 |- (B =/= suc y <-> -. B = suc y)
60	59	anbi2i 482	. . . . . . . 8 |- ((B (_ suc y /\ B =/= suc y) <-> (B (_ suc y /\ -. B = suc y))
61		annim 236	. . . . . . . 8 |- ((B (_ suc y /\ -. B = suc y) <-> -. (B (_ suc y -> B = suc y))
62	60, 61	bitri 171	. . . . . . 7 |- ((B (_ suc y /\ B =/= suc y) <-> -. (B (_ suc y -> B = suc y))
63	58, 62	syl5ibr 205	. . . . . 6 |- ((y e. om /\ B e. om) -> (-. (B (_ suc y -> B = suc y) -> ((B (_ y -> ch) -> (B (_ suc y -> th))))
64	42, 63	pm2.61d 125	. . . . 5 |- ((y e. om /\ B e. om) -> ((B (_ y -> ch) -> (B (_ suc y -> th)))
65	64	ex 371	. . . 4 |- (y e. om -> (B e. om -> ((B (_ y -> ch) -> (B (_ suc y -> th))))
66	65	a2d 13	. . 3 |- (y e. om -> ((B e. om -> (B (_ y -> ch)) -> (B e. om -> (B (_ suc y -> th))))
67	15, 19, 23, 27, 29, 66	finds 3218	. 2 |- (A e. om -> (B e. om -> (B (_ A -> ta)))
68	67	imp31 360	1 |- (((A e. om /\ B e. om) /\ B (_ A) -> ta)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 144   /\ wa 221   = wceq 988   e. wcel 990  E.wex 1012   =/= wne 1622   (_ wss 2091  (/)c0 2324  Oncon0 3003  suc csuc 3005  omcom 3192

This theorem is referenced by:  inf3lem5 4703  indpi 5123

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-9 997  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-nul 2761  ax-pow 2794  ax-pr 2832  ax-un 2920

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 779  df-3an 780  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-ral 1687  df-rex 1688  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-if 2407  df-pw 2447  df-sn 2457  df-pr 2458  df-tp 2460  df-op 2461  df-uni 2552  df-br 2670  df-opab 2718  df-tr 2732  df-eprel 2886  df-po 2894  df-so 2904  df-fr 2972  df-we 2989  df-ord 3006  df-on 3007  df-lim 3008  df-suc 3009  df-om 3193

Copyright terms: Public domain