Theorem tfindsg 6698

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
tfindsg	|- ( ( ( A e. On /\ B e. On ) /\ B C_ 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 tfindsg

Step	Hyp	Ref	Expression
1		sseq2 3486	. . . . . . 7 |- ( x = (/) -> ( B C_ x <-> B C_ (/) ) )
2	1	adantl 467	. . . . . 6 |- ( ( B = (/) /\ x = (/) ) -> ( B C_ x <-> B C_ (/) ) )
3		eqeq2 2437	. . . . . . . 8 |- ( B = (/) -> ( x = B <-> x = (/) ) )
4		tfindsg.1	. . . . . . . 8 |- ( x = B -> ( ph <-> ps ) )
5	3, 4	syl6bir 232	. . . . . . 7 |- ( B = (/) -> ( x = (/) -> ( ph <-> ps ) ) )
6	5	imp 430	. . . . . 6 |- ( ( B = (/) /\ x = (/) ) -> ( ph <-> ps ) )
7	2, 6	imbi12d 321	. . . . 5 |- ( ( B = (/) /\ x = (/) ) -> ( ( B C_ x -> ph ) <-> ( B C_ (/) -> ps ) ) )
8	1	imbi1d 318	. . . . . 6 |- ( x = (/) -> ( ( B C_ x -> ph ) <-> ( B C_ (/) -> ph ) ) )
9		ss0 3793	. . . . . . . . 9 |- ( B C_ (/) -> B = (/) )
10	9	con3i 140	. . . . . . . 8 |- ( -. B = (/) -> -. B C_ (/) )
11	10	pm2.21d 109	. . . . . . 7 |- ( -. B = (/) -> ( B C_ (/) -> ( ph <-> ps ) ) )
12	11	pm5.74d 250	. . . . . 6 |- ( -. B = (/) -> ( ( B C_ (/) -> ph ) <-> ( B C_ (/) -> ps ) ) )
13	8, 12	sylan9bbr 705	. . . . 5 |- ( ( -. B = (/) /\ x = (/) ) -> ( ( B C_ x -> ph ) <-> ( B C_ (/) -> ps ) ) )
14	7, 13	pm2.61ian 797	. . . 4 |- ( x = (/) -> ( ( B C_ x -> ph ) <-> ( B C_ (/) -> ps ) ) )
15	14	imbi2d 317	. . 3 |- ( x = (/) -> ( ( B e. On -> ( B C_ x -> ph ) ) <-> ( B e. On -> ( B C_ (/) -> ps ) ) ) )
16		sseq2 3486	. . . . 5 |- ( x = y -> ( B C_ x <-> B C_ y ) )
17		tfindsg.2	. . . . 5 |- ( x = y -> ( ph <-> ch ) )
18	16, 17	imbi12d 321	. . . 4 |- ( x = y -> ( ( B C_ x -> ph ) <-> ( B C_ y -> ch ) ) )
19	18	imbi2d 317	. . 3 |- ( x = y -> ( ( B e. On -> ( B C_ x -> ph ) ) <-> ( B e. On -> ( B C_ y -> ch ) ) ) )
20		sseq2 3486	. . . . 5 |- ( x = suc y -> ( B C_ x <-> B C_ suc y ) )
21		tfindsg.3	. . . . 5 |- ( x = suc y -> ( ph <-> th ) )
22	20, 21	imbi12d 321	. . . 4 |- ( x = suc y -> ( ( B C_ x -> ph ) <-> ( B C_ suc y -> th ) ) )
23	22	imbi2d 317	. . 3 |- ( x = suc y -> ( ( B e. On -> ( B C_ x -> ph ) ) <-> ( B e. On -> ( B C_ suc y -> th ) ) ) )
24		sseq2 3486	. . . . 5 |- ( x = A -> ( B C_ x <-> B C_ A ) )
25		tfindsg.4	. . . . 5 |- ( x = A -> ( ph <-> ta ) )
26	24, 25	imbi12d 321	. . . 4 |- ( x = A -> ( ( B C_ x -> ph ) <-> ( B C_ A -> ta ) ) )
27	26	imbi2d 317	. . 3 |- ( x = A -> ( ( B e. On -> ( B C_ x -> ph ) ) <-> ( B e. On -> ( B C_ A -> ta ) ) ) )
28		tfindsg.5	. . . 4 |- ( B e. On -> ps )
29	28	a1d 26	. . 3 |- ( B e. On -> ( B C_ (/) -> ps ) )
30		vex 3084	. . . . . . . . . . . . . 14 |- y e. _V
31	30	sucex 6649	. . . . . . . . . . . . 13 |- suc y e. _V
32	31	eqvinc 3198	. . . . . . . . . . . 12 |- ( suc y = B <-> E. x ( x = suc y /\ x = B ) )
33	28, 4	syl5ibr 224	. . . . . . . . . . . . . 14 |- ( x = B -> ( B e. On -> ph ) )
34	21	biimpd 210	. . . . . . . . . . . . . 14 |- ( x = suc y -> ( ph -> th ) )
35	33, 34	sylan9r 662	. . . . . . . . . . . . 13 |- ( ( x = suc y /\ x = B ) -> ( B e. On -> th ) )
36	35	exlimiv 1766	. . . . . . . . . . . 12 |- ( E. x ( x = suc y /\ x = B ) -> ( B e. On -> th ) )
37	32, 36	sylbi 198	. . . . . . . . . . 11 |- ( suc y = B -> ( B e. On -> th ) )
38	37	eqcoms 2434	. . . . . . . . . 10 |- ( B = suc y -> ( B e. On -> th ) )
39	38	imim2i 16	. . . . . . . . 9 |- ( ( B C_ suc y -> B = suc y ) -> ( B C_ suc y -> ( B e. On -> th ) ) )
40	39	a1d 26	. . . . . . . 8 |- ( ( B C_ suc y -> B = suc y ) -> ( ( B C_ y -> ch ) -> ( B C_ suc y -> ( B e. On -> th ) ) ) )
41	40	com4r 89	. . . . . . 7 |- ( B e. On -> ( ( B C_ suc y -> B = suc y ) -> ( ( B C_ y -> ch ) -> ( B C_ suc y -> th ) ) ) )
42	41	adantl 467	. . . . . 6 |- ( ( y e. On /\ B e. On ) -> ( ( B C_ suc y -> B = suc y ) -> ( ( B C_ y -> ch ) -> ( B C_ suc y -> th ) ) ) )
43		df-ne 2620	. . . . . . . . 9 |- ( B =/= suc y <-> -. B = suc y )
44	43	anbi2i 698	. . . . . . . 8 |- ( ( B C_ suc y /\ B =/= suc y ) <-> ( B C_ suc y /\ -. B = suc y ) )
45		annim 426	. . . . . . . 8 |- ( ( B C_ suc y /\ -. B = suc y ) <-> -. ( B C_ suc y -> B = suc y ) )
46	44, 45	bitri 252	. . . . . . 7 |- ( ( B C_ suc y /\ B =/= suc y ) <-> -. ( B C_ suc y -> B = suc y ) )
47		onsssuc 5526	. . . . . . . . . 10 |- ( ( B e. On /\ y e. On ) -> ( B C_ y <-> B e. suc y ) )
48		suceloni 6651	. . . . . . . . . . 11 |- ( y e. On -> suc y e. On )
49		onelpss 5479	. . . . . . . . . . 11 |- ( ( B e. On /\ suc y e. On ) -> ( B e. suc y <-> ( B C_ suc y /\ B =/= suc y ) ) )
50	48, 49	sylan2 476	. . . . . . . . . 10 |- ( ( B e. On /\ y e. On ) -> ( B e. suc y <-> ( B C_ suc y /\ B =/= suc y ) ) )
51	47, 50	bitrd 256	. . . . . . . . 9 |- ( ( B e. On /\ y e. On ) -> ( B C_ y <-> ( B C_ suc y /\ B =/= suc y ) ) )
52	51	ancoms 454	. . . . . . . 8 |- ( ( y e. On /\ B e. On ) -> ( B C_ y <-> ( B C_ suc y /\ B =/= suc y ) ) )
53		tfindsg.6	. . . . . . . . . . . 12 |- ( ( ( y e. On /\ B e. On ) /\ B C_ y ) -> ( ch -> th ) )
54	53	ex 435	. . . . . . . . . . 11 |- ( ( y e. On /\ B e. On ) -> ( B C_ y -> ( ch -> th ) ) )
55		ax-1 6	. . . . . . . . . . 11 |- ( th -> ( B C_ suc y -> th ) )
56	54, 55	syl8 72	. . . . . . . . . 10 |- ( ( y e. On /\ B e. On ) -> ( B C_ y -> ( ch -> ( B C_ suc y -> th ) ) ) )
57	56	a2d 29	. . . . . . . . 9 |- ( ( y e. On /\ B e. On ) -> ( ( B C_ y -> ch ) -> ( B C_ y -> ( B C_ suc y -> th ) ) ) )
58	57	com23 81	. . . . . . . 8 |- ( ( y e. On /\ B e. On ) -> ( B C_ y -> ( ( B C_ y -> ch ) -> ( B C_ suc y -> th ) ) ) )
59	52, 58	sylbird 238	. . . . . . 7 |- ( ( y e. On /\ B e. On ) -> ( ( B C_ suc y /\ B =/= suc y ) -> ( ( B C_ y -> ch ) -> ( B C_ suc y -> th ) ) ) )
60	46, 59	syl5bir 221	. . . . . 6 |- ( ( y e. On /\ B e. On ) -> ( -. ( B C_ suc y -> B = suc y ) -> ( ( B C_ y -> ch ) -> ( B C_ suc y -> th ) ) ) )
61	42, 60	pm2.61d 161	. . . . 5 |- ( ( y e. On /\ B e. On ) -> ( ( B C_ y -> ch ) -> ( B C_ suc y -> th ) ) )
62	61	ex 435	. . . 4 |- ( y e. On -> ( B e. On -> ( ( B C_ y -> ch ) -> ( B C_ suc y -> th ) ) ) )
63	62	a2d 29	. . 3 |- ( y e. On -> ( ( B e. On -> ( B C_ y -> ch ) ) -> ( B e. On -> ( B C_ suc y -> th ) ) ) )
64		pm2.27 40	. . . . . . . . 9 |- ( B e. On -> ( ( B e. On -> ( B C_ y -> ch ) ) -> ( B C_ y -> ch ) ) )
65	64	ralimdv 2835	. . . . . . . 8 |- ( 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 731	. . . . . . 7 |- ( ( ( 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		tfindsg.7	. . . . . . 7 |- ( ( ( Lim x /\ B e. On ) /\ B C_ x ) -> ( A. y e. x ( B C_ y -> ch ) -> ph ) )
68	66, 67	syld 45	. . . . . 6 |- ( ( ( Lim x /\ B e. On ) /\ B C_ x ) -> ( A. y e. x ( B e. On -> ( B C_ y -> ch ) ) -> ph ) )
69	68	exp31 607	. . . . 5 |- ( Lim x -> ( B e. On -> ( B C_ x -> ( A. y e. x ( B e. On -> ( B C_ y -> ch ) ) -> ph ) ) ) )
70	69	com3l 84	. . . 4 |- ( B e. On -> ( B C_ x -> ( Lim x -> ( A. y e. x ( B e. On -> ( B C_ y -> ch ) ) -> ph ) ) ) )
71	70	com4t 88	. . 3 |- ( Lim x -> ( A. y e. x ( B e. On -> ( B C_ y -> ch ) ) -> ( B e. On -> ( B C_ x -> ph ) ) ) )
72	15, 19, 23, 27, 29, 63, 71	tfinds 6697	. 2 |- ( A e. On -> ( B e. On -> ( B C_ A -> ta ) ) )
73	72	imp31 433	1 |- ( ( ( A e. On /\ B e. On ) /\ B C_ A ) -> ta )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   E.wex 1659   e. wcel 1868   =/= wne 2618   A.wral 2775   C_ wss 3436   (/)c0 3761   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:  tfindsg2  6699  oaordi  7252  infensuc  7753  r1ordg  8251