Theorem tfindsg2 6699

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 suc B instead of zero. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 5-Jan-2005.)

Hypotheses

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

Assertion

Ref	Expression
tfindsg2	|- ( ( A e. On /\ B e. A ) -> ta )

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

Allowed substitution hints:   ph( x)   ps( x, y)   ch( y)   th( y)   ta( y)   A( y)

Proof of Theorem tfindsg2

Step	Hyp	Ref	Expression
1		onelon 5464	. . 3 |- ( ( A e. On /\ B e. A ) -> B e. On )
2		sucelon 6655	. . 3 |- ( B e. On <-> suc B e. On )
3	1, 2	sylib 199	. 2 |- ( ( A e. On /\ B e. A ) -> suc B e. On )
4		eloni 5449	. . . 4 |- ( A e. On -> Ord A )
5		ordsucss 6656	. . . 4 |- ( Ord A -> ( B e. A -> suc B C_ A ) )
6	4, 5	syl 17	. . 3 |- ( A e. On -> ( B e. A -> suc B C_ A ) )
7	6	imp 430	. 2 |- ( ( A e. On /\ B e. A ) -> suc B C_ A )
8		tfindsg2.1	. . . . 5 |- ( x = suc B -> ( ph <-> ps ) )
9		tfindsg2.2	. . . . 5 |- ( x = y -> ( ph <-> ch ) )
10		tfindsg2.3	. . . . 5 |- ( x = suc y -> ( ph <-> th ) )
11		tfindsg2.4	. . . . 5 |- ( x = A -> ( ph <-> ta ) )
12		tfindsg2.5	. . . . . 6 |- ( B e. On -> ps )
13	2, 12	sylbir 216	. . . . 5 |- ( suc B e. On -> ps )
14		eloni 5449	. . . . . . . . . 10 |- ( y e. On -> Ord y )
15		ordelsuc 6658	. . . . . . . . . 10 |- ( ( B e. On /\ Ord y ) -> ( B e. y <-> suc B C_ y ) )
16	14, 15	sylan2 476	. . . . . . . . 9 |- ( ( B e. On /\ y e. On ) -> ( B e. y <-> suc B C_ y ) )
17	16	ancoms 454	. . . . . . . 8 |- ( ( y e. On /\ B e. On ) -> ( B e. y <-> suc B C_ y ) )
18		tfindsg2.6	. . . . . . . . . 10 |- ( ( y e. On /\ B e. y ) -> ( ch -> th ) )
19	18	ex 435	. . . . . . . . 9 |- ( y e. On -> ( B e. y -> ( ch -> th ) ) )
20	19	adantr 466	. . . . . . . 8 |- ( ( y e. On /\ B e. On ) -> ( B e. y -> ( ch -> th ) ) )
21	17, 20	sylbird 238	. . . . . . 7 |- ( ( y e. On /\ B e. On ) -> ( suc B C_ y -> ( ch -> th ) ) )
22	2, 21	sylan2br 478	. . . . . 6 |- ( ( y e. On /\ suc B e. On ) -> ( suc B C_ y -> ( ch -> th ) ) )
23	22	imp 430	. . . . 5 |- ( ( ( y e. On /\ suc B e. On ) /\ suc B C_ y ) -> ( ch -> th ) )
24		tfindsg2.7	. . . . . . . . . 10 |- ( ( Lim x /\ B e. x ) -> ( A. y e. x ( B e. y -> ch ) -> ph ) )
25	24	ex 435	. . . . . . . . 9 |- ( Lim x -> ( B e. x -> ( A. y e. x ( B e. y -> ch ) -> ph ) ) )
26	25	adantr 466	. . . . . . . 8 |- ( ( Lim x /\ B e. On ) -> ( B e. x -> ( A. y e. x ( B e. y -> ch ) -> ph ) ) )
27		vex 3084	. . . . . . . . . . 11 |- x e. _V
28		limelon 5502	. . . . . . . . . . 11 |- ( ( x e. _V /\ Lim x ) -> x e. On )
29	27, 28	mpan 674	. . . . . . . . . 10 |- ( Lim x -> x e. On )
30		eloni 5449	. . . . . . . . . . . 12 |- ( x e. On -> Ord x )
31		ordelsuc 6658	. . . . . . . . . . . 12 |- ( ( B e. On /\ Ord x ) -> ( B e. x <-> suc B C_ x ) )
32	30, 31	sylan2 476	. . . . . . . . . . 11 |- ( ( B e. On /\ x e. On ) -> ( B e. x <-> suc B C_ x ) )
33		onelon 5464	. . . . . . . . . . . . . . . . 17 |- ( ( x e. On /\ y e. x ) -> y e. On )
34	33, 14	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( x e. On /\ y e. x ) -> Ord y )
35	34, 15	sylan2 476	. . . . . . . . . . . . . . 15 |- ( ( B e. On /\ ( x e. On /\ y e. x ) ) -> ( B e. y <-> suc B C_ y ) )
36	35	anassrs 652	. . . . . . . . . . . . . 14 |- ( ( ( B e. On /\ x e. On ) /\ y e. x ) -> ( B e. y <-> suc B C_ y ) )
37	36	imbi1d 318	. . . . . . . . . . . . 13 |- ( ( ( B e. On /\ x e. On ) /\ y e. x ) -> ( ( B e. y -> ch ) <-> ( suc B C_ y -> ch ) ) )
38	37	ralbidva 2861	. . . . . . . . . . . 12 |- ( ( B e. On /\ x e. On ) -> ( A. y e. x ( B e. y -> ch ) <-> A. y e. x ( suc B C_ y -> ch ) ) )
39	38	imbi1d 318	. . . . . . . . . . 11 |- ( ( B e. On /\ x e. On ) -> ( ( A. y e. x ( B e. y -> ch ) -> ph ) <-> ( A. y e. x ( suc B C_ y -> ch ) -> ph ) ) )
40	32, 39	imbi12d 321	. . . . . . . . . 10 |- ( ( B e. On /\ x e. On ) -> ( ( B e. x -> ( A. y e. x ( B e. y -> ch ) -> ph ) ) <-> ( suc B C_ x -> ( A. y e. x ( suc B C_ y -> ch ) -> ph ) ) ) )
41	29, 40	sylan2 476	. . . . . . . . 9 |- ( ( B e. On /\ Lim x ) -> ( ( B e. x -> ( A. y e. x ( B e. y -> ch ) -> ph ) ) <-> ( suc B C_ x -> ( A. y e. x ( suc B C_ y -> ch ) -> ph ) ) ) )
42	41	ancoms 454	. . . . . . . 8 |- ( ( Lim x /\ B e. On ) -> ( ( B e. x -> ( A. y e. x ( B e. y -> ch ) -> ph ) ) <-> ( suc B C_ x -> ( A. y e. x ( suc B C_ y -> ch ) -> ph ) ) ) )
43	26, 42	mpbid 213	. . . . . . 7 |- ( ( Lim x /\ B e. On ) -> ( suc B C_ x -> ( A. y e. x ( suc B C_ y -> ch ) -> ph ) ) )
44	2, 43	sylan2br 478	. . . . . 6 |- ( ( Lim x /\ suc B e. On ) -> ( suc B C_ x -> ( A. y e. x ( suc B C_ y -> ch ) -> ph ) ) )
45	44	imp 430	. . . . 5 |- ( ( ( Lim x /\ suc B e. On ) /\ suc B C_ x ) -> ( A. y e. x ( suc B C_ y -> ch ) -> ph ) )
46	8, 9, 10, 11, 13, 23, 45	tfindsg 6698	. . . 4 |- ( ( ( A e. On /\ suc B e. On ) /\ suc B C_ A ) -> ta )
47	46	expl 622	. . 3 |- ( A e. On -> ( ( suc B e. On /\ suc B C_ A ) -> ta ) )
48	47	adantr 466	. 2 |- ( ( A e. On /\ B e. A ) -> ( ( suc B e. On /\ suc B C_ A ) -> ta ) )
49	3, 7, 48	mp2and 683	1 |- ( ( A e. On /\ B e. A ) -> ta )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   e. wcel 1868   A.wral 2775   _Vcvv 3081   C_ wss 3436   Ord word 5438   Oncon0 5439   Lim wlim 5440   suc csuc 5441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657  ax-un 6594

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-tr 4516  df-eprel 4761  df-po 4771  df-so 4772  df-fr 4809  df-we 4811  df-ord 5442  df-on 5443  df-lim 5444  df-suc 5445

This theorem is referenced by:  oeordi  7293