Theorem tfindsg 3157

Description: Transfinite Induction (inference schema) with implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction hypothesis for successors, and the induction hypothesis for limit ordinals. The basis of this version is an arbitrary ordinal B instead of zero. Remark in [TakeutiZaring] p. 57.

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 (_ y) -> (ch -> th))
tfindsg.7	|- (((Lim x /\ B e. On) /\ B (_ x) -> (A.y e. x (B (_ y -> ch) -> ph))

Assertion

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

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

Proof of Theorem tfindsg

Step	Hyp	Ref	Expression
1		sseq2 2079	. . . . . . 7 |- (x = (/) -> (B (_ x <-> B (_ (/)))
2	1	adantl 388	. . . . . 6 |- ((B = (/) /\ x = (/)) -> (B (_ x <-> B (_ (/)))
3		eqeq2 1481	. . . . . . . 8 |- (B = (/) -> (x = B <-> x = (/)))
4		tfindsg.1	. . . . . . . 8 |- (x = B -> (ph <-> ps))
5	3, 4	syl6bir 215	. . . . . . 7 |- (B = (/) -> (x = (/) -> (ph <-> ps)))
6	5	imp 350	. . . . . 6 |- ((B = (/) /\ x = (/)) -> (ph <-> ps))
7	2, 6	imbi12d 625	. . . . 5 |- ((B = (/) /\ x = (/)) -> ((B (_ x -> ph) <-> (B (_ (/) -> ps)))
8	1	imbi1d 612	. . . . . 6 |- (x = (/) -> ((B (_ x -> ph) <-> (B (_ (/) -> ph)))
9		ss0 2299	. . . . . . . . 9 |- (B (_ (/) -> B = (/))
10	9	con3i 98	. . . . . . . 8 |- (-. B = (/) -> -. B (_ (/))
11	10	pm2.21d 78	. . . . . . 7 |- (-. B = (/) -> (B (_ (/) -> (ph <-> ps)))
12	11	pm5.74d 584	. . . . . 6 |- (-. B = (/) -> ((B (_ (/) -> ph) <-> (B (_ (/) -> ps)))
13	8, 12	sylan9bbr 540	. . . . 5 |- ((-. B = (/) /\ x = (/)) -> ((B (_ x -> ph) <-> (B (_ (/) -> ps)))
14	7, 13	pm2.61ian 476	. . . 4 |- (x = (/) -> ((B (_ x -> ph) <-> (B (_ (/) -> ps)))
15	14	imbi2d 611	. . 3 |- (x = (/) -> ((B e. On -> (B (_ x -> ph)) <-> (B e. On -> (B (_ (/) -> ps))))
16		sseq2 2079	. . . . 5 |- (x = y -> (B (_ x <-> B (_ y))
17		tfindsg.2	. . . . 5 |- (x = y -> (ph <-> ch))
18	16, 17	imbi12d 625	. . . 4 |- (x = y -> ((B (_ x -> ph) <-> (B (_ y -> ch)))
19	18	imbi2d 611	. . 3 |- (x = y -> ((B e. On -> (B (_ x -> ph)) <-> (B e. On -> (B (_ y -> ch))))
20		sseq2 2079	. . . . 5 |- (x = suc y -> (B (_ x <-> B (_ suc y))
21		tfindsg.3	. . . . 5 |- (x = suc y -> (ph <-> th))
22	20, 21	imbi12d 625	. . . 4 |- (x = suc y -> ((B (_ x -> ph) <-> (B (_ suc y -> th)))
23	22	imbi2d 611	. . 3 |- (x = suc y -> ((B e. On -> (B (_ x -> ph)) <-> (B e. On -> (B (_ suc y -> th))))
24		sseq2 2079	. . . . 5 |- (x = A -> (B (_ x <-> B (_ A))
25		tfindsg.4	. . . . 5 |- (x = A -> (ph <-> ta))
26	24, 25	imbi12d 625	. . . 4 |- (x = A -> ((B (_ x -> ph) <-> (B (_ A -> ta)))
27	26	imbi2d 611	. . 3 |- (x = A -> ((B e. On -> (B (_ x -> ph)) <-> (B e. On -> (B (_ A -> ta))))
28		tfindsg.5	. . . 4 |- (B e. On -> ps)
29	28	a1d 12	. . 3 |- (B e. On -> (B (_ (/) -> ps))
30		visset 1809	. . . . . . . . . . . . . 14 |- y e. V
31	30	sucex 3045	. . . . . . . . . . . . 13 |- suc y e. V
32	31	eqvinc 1879	. . . . . . . . . . . 12 |- (suc y = B <-> E.x(x = suc y /\ x = B))
33	4, 28	syl5bir 210	. . . . . . . . . . . . . 14 |- (x = B -> (B e. On -> ph))
34	21	biimpd 153	. . . . . . . . . . . . . 14 |- (x = suc y -> (ph -> th))
35	33, 34	sylan9r 469	. . . . . . . . . . . . 13 |- ((x = suc y /\ x = B) -> (B e. On -> th))
36	35	19.23aiv 1293	. . . . . . . . . . . 12 |- (E.x(x = suc y /\ x = B) -> (B e. On -> th))
37	32, 36	sylbi 199	. . . . . . . . . . 11 |- (suc y = B -> (B e. On -> th))
38	37	eqcoms 1475	. . . . . . . . . 10 |- (B = suc y -> (B e. On -> th))
39	38	imim2i 17	. . . . . . . . 9 |- ((B (_ suc y -> B = suc y) -> (B (_ suc y -> (B e. On -> th)))
40	39	a1d 12	. . . . . . . 8 |- ((B (_ suc y -> B = suc y) -> ((B (_ y -> ch) -> (B (_ suc y -> (B e. On -> th))))
41	40	com4r 41	. . . . . . 7 |- (B e. On -> ((B (_ suc y -> B = suc y) -> ((B (_ y -> ch) -> (B (_ suc y -> th))))
42	41	adantl 388	. . . . . 6 |- ((y e. On /\ B e. On) -> ((B (_ suc y -> B = suc y) -> ((B (_ y -> ch) -> (B (_ suc y -> th))))
43		onsssuc 3053	. . . . . . . . . 10 |- ((B e. On /\ y e. On) -> (B (_ y <-> B e. suc y))
44		onelpsst 2993	. . . . . . . . . . 11 |- ((B e. On /\ suc y e. On) -> (B e. suc y <-> (B (_ suc y /\ B =/= suc y)))
45		suceloni 3057	. . . . . . . . . . 11 |- (y e. On -> suc y e. On)
46	44, 45	sylan2 451	. . . . . . . . . 10 |- ((B e. On /\ y e. On) -> (B e. suc y <-> (B (_ suc y /\ B =/= suc y)))
47	43, 46	bitrd 527	. . . . . . . . 9 |- ((B e. On /\ y e. On) -> (B (_ y <-> (B (_ suc y /\ B =/= suc y)))
48	47	ancoms 436	. . . . . . . 8 |- ((y e. On /\ B e. On) -> (B (_ y <-> (B (_ suc y /\ B =/= suc y)))
49		tfindsg.6	. . . . . . . . . . . 12 |- (((y e. On /\ B e. On) /\ B (_ y) -> (ch -> th))
50	49	ex 373	. . . . . . . . . . 11 |- ((y e. On /\ B e. On) -> (B (_ y -> (ch -> th)))
51		ax-1 4	. . . . . . . . . . 11 |- (th -> (B (_ suc y -> th))
52	50, 51	syl8 24	. . . . . . . . . 10 |- ((y e. On /\ B e. On) -> (B (_ y -> (ch -> (B (_ suc y -> th))))
53	52	a2d 13	. . . . . . . . 9 |- ((y e. On /\ B e. On) -> ((B (_ y -> ch) -> (B (_ y -> (B (_ suc y -> th))))
54	53	com23 32	. . . . . . . 8 |- ((y e. On /\ B e. On) -> (B (_ y -> ((B (_ y -> ch) -> (B (_ suc y -> th))))
55	48, 54	sylbird 205	. . . . . . 7 |- ((y e. On /\ B e. On) -> ((B (_ suc y /\ B =/= suc y) -> ((B (_ y -> ch) -> (B (_ suc y -> th))))
56		df-ne 1584	. . . . . . . . 9 |- (B =/= suc y <-> -. B = suc y)
57	56	anbi2i 480	. . . . . . . 8 |- ((B (_ suc y /\ B =/= suc y) <-> (B (_ suc y /\ -. B = suc y))
58		annim 238	. . . . . . . 8 |- ((B (_ suc y /\ -. B = suc y) <-> -. (B (_ suc y -> B = suc y))
59	57, 58	bitr 173	. . . . . . 7 |- ((B (_ suc y /\ B =/= suc y) <-> -. (B (_ suc y -> B = suc y))
60	55, 59	syl5ibr 207	. . . . . 6 |- ((y e. On /\ B e. On) -> (-. (B (_ suc y -> B = suc y) -> ((B (_ y -> ch) -> (B (_ suc y -> th))))
61	42, 60	pm2.61d 127	. . . . 5 |- ((y e. On /\ B e. On) -> ((B (_ y -> ch) -> (B (_ suc y -> th)))
62	61	ex 373	. . . 4 |- (y e. On -> (B e. On -> ((B (_ y -> ch) -> (B (_ suc y -> th))))
63	62	a2d 13	. . 3 |- (y e. On -> ((B e. On -> (B (_ y -> ch)) -> (B e. On -> (B (_ suc y -> th))))
64		pm2.27 62	. . . . . . . . 9 |- (B e. On -> ((B e. On -> (B (_ y -> ch)) -> (B (_ y -> ch)))
65	64	r19.20sdv 1707	. . . . . . . 8 |- (B e. On -> (A.y e. x (B e. On -> (B (_ y -> ch)) -> A.y e. x (B (_ y -> ch)))
66	65	ad2antlr 405	. . . . . . 7 |- (((Lim x /\ B e. On) /\ B (_ x) -> (A.y e. x (B e. On -> (B (_ y -> ch)) -> A.y e. x (B (_ y -> ch)))
67		tfindsg.7	. . . . . . 7 |- (((Lim x /\ B e. On) /\ B (_ x) -> (A.y e. x (B (_ y -> ch) -> ph))
68	66, 67	syld 27	. . . . . 6 |- (((Lim x /\ B e. On) /\ B (_ x) -> (A.y e. x (B e. On -> (B (_ y -> ch)) -> ph))
69	68	exp31 376	. . . . 5 |- (Lim x -> (B e. On -> (B (_ x -> (A.y e. x (B e. On -> (B (_ y -> ch)) -> ph))))
70	69	com3l 34	. . . 4 |- (B e. On -> (B (_ x -> (Lim x -> (A.y e. x (B e. On -> (B (_ y -> ch)) -> ph))))
71	70	com4t 40	. . 3 |- (Lim x -> (A.y e. x (B e. On ->