Theorem tz7.44-2 3924

Description: The value of F at a successor ordinal. Part 2 of Theorem 7.44 of [TakeutiZaring] p. 49.

Hypotheses

Ref	Expression
tz7.44.1	|- G = {<.x, y>. | ((x = (/) /\ y = A) \/ (-. (x = (/) \/ Lim dom x) /\ y = (H` (x` U.dom x))) \/ (Lim dom x /\ y = U.ran x))}
tz7.44.2	|- F Fn On
tz7.44.3	|- (x e. On -> (F` x) = (G` (F |` x)))
tz7.44.5	|- B e. On

Assertion

Ref	Expression
tz7.44-2	|- (F` suc B) = (H` (F` B))

Distinct variable groups:   x,y,A   x,F   x,G   y,H   x,B,y   y,F   x,H

Proof of Theorem tz7.44-2

Step	Hyp	Ref	Expression
1		tz7.44.5	. . . 4 |- B e. On
2	1	onsuc 3101	. . 3 |- suc B e. On
3		fveq2 3719	. . . . 5 |- (x = suc B -> (F` x) = (F` suc B))
4		reseq2 3365	. . . . . 6 |- (x = suc B -> (F |` x) = (F |` suc B))
5	4	fveq2d 3723	. . . . 5 |- (x = suc B -> (G` (F |` x)) = (G` (F |` suc B)))
6	3, 5	eqeq12d 1487	. . . 4 |- (x = suc B -> ((F` x) = (G` (F |` x)) <-> (F` suc B) = (G` (F |` suc B))))
7		tz7.44.3	. . . 4 |- (x e. On -> (F` x) = (G` (F |` x)))
8	6, 7	vtoclga 1849	. . 3 |- (suc B e. On -> (F` suc B) = (G` (F |` suc B)))
9	2, 8	ax-mp 7	. 2 |- (F` suc B) = (G` (F |` suc B))
10		tz7.44.1	. . . 4 |- G = {<.x, y>. | ((x = (/) /\ y = A) \/ (-. (x = (/) \/ Lim dom x) /\ y = (H` (x` U.dom x))) \/ (Lim dom x /\ y = U.ran x))}
11	10	tz7.44lem1 3922	. . 3 |- Fun G
12		3mix2 815	. . . . . 6 |- ((-. (x = (/) \/ Lim dom x) /\ y = (H` (x` U.dom x))) -> ((x = (/) /\ y = A) \/ (-. (x = (/) \/ Lim dom x) /\ y = (H` (x` U.dom x))) \/ (Lim dom x /\ y = U.ran x)))
13	12	ssopab2i 2819	. . . . 5 |- {<.x, y>. | (-. (x = (/) \/ Lim dom x) /\ y = (H` (x` U.dom x)))} (_ {<.x, y>. | ((x = (/) /\ y = A) \/ (-. (x = (/) \/ Lim dom x) /\ y = (H` (x` U.dom x))) \/ (Lim dom x /\ y = U.ran x))}
14	13, 10	sseqtr4 2091	. . . 4 |- {<.x, y>. | (-. (x = (/) \/ Lim dom x) /\ y = (H` (x` U.dom x)))} (_ G
15		tz7.44.2	. . . . . . . 8 |- F Fn On
16		fnfun 3581	. . . . . . . 8 |- (F Fn On -> Fun F)
17	15, 16	ax-mp 7	. . . . . . 7 |- Fun F
18		resfunexg 3575	. . . . . . 7 |- ((Fun F /\ suc B e. On) -> (F |` suc B) e. V)
19	17, 2, 18	mp2an 696	. . . . . 6 |- (F |` suc B) e. V
20		fvex 3727	. . . . . 6 |- (H` (F` B)) e. V
21		eqeq1 1479	. . . . . . . . 9 |- (x = (F |` suc B) -> (x = (/) <-> (F |` suc B) = (/)))
22		dmeq 3307	. . . . . . . . . 10 |- (x = (F |` suc B) -> dom x = dom ( F |` suc B))
23		limeq 2956	. . . . . . . . . 10 |- (dom x = dom ( F |` suc B) -> (Lim dom x <-> Lim dom ( F |` suc B)))
24	22, 23	syl 10	. . . . . . . . 9 |- (x = (F |` suc B) -> (Lim dom x <-> Lim dom ( F |` suc B)))
25	21, 24	orbi12d 626	. . . . . . . 8 |- (x = (F |` suc B) -> ((x = (/) \/ Lim dom x) <-> ((F |` suc B) = (/) \/ Lim dom ( F |` suc B))))
26	25	negbid 610	. . . . . . 7 |- (x = (F |` suc B) -> (-. (x = (/) \/ Lim dom x) <-> -. ((F |` suc B) = (/) \/ Lim dom ( F |` suc B))))
27		unieq 2506	. . . . . . . . . . 11 |- (dom x = dom ( F |` suc B) -> U.dom x = U.dom ( F |` suc B))
28		fveq2 3719	. . . . . . . . . . 11 |- (U.dom x = U.dom ( F |` suc B) -> (x` U.dom x) = (x` U.dom ( F |` suc B)))
29	22, 27, 28	3syl 20	. . . . . . . . . 10 |- (x = (F |` suc B) -> (x` U.dom x) = (x` U.dom ( F |` suc B)))
30		fveq1 3718	. . . . . . . . . 10 |- (x = (F |` suc B) -> (x` U.dom ( F |` suc B)) = ((F |` suc B)` U.dom ( F |` suc B)))
31	29, 30	eqtrd 1505	. . . . . . . . 9 |- (x = (F |` suc B) -> (x` U.dom x) = ((F |` suc B)` U.dom ( F |` suc B)))
32	31	fveq2d 3723	. . . . . . . 8 |- (x = (F |` suc B) -> (H` (x` U.dom x)) = (H` ((F |` suc B)` U.dom ( F |` suc B))))
33	32	eqeq2d 1484	. . . . . . 7 |- (x = (F |` suc B) -> (y = (H` (x` U.dom x)) <-> y = (H` ((F |` suc B)` U.dom ( F |` suc B)))))
34	26, 33	anbi12d 627	. . . . . 6 |- (x = (F |` suc B) -> ((-. (x = (/) \/ Lim dom x) /\ y = (H` (x` U.dom x))) <-> (-. ((F |` suc B) = (/) \/ Lim dom ( F |` suc B)) /\ y = (H` ((F |` suc B)` U.dom ( F |` suc B))))))
35		eqeq1 1479	. . . . . . 7 |- (y = (H` (F` B)) -> (y = (H` ((F |` suc B)` U.dom ( F |` suc B))) <-> (H` (F` B)) = (H` ((F |` suc B)` U.dom ( F |` suc B)))))
36	35	anbi2d 615	. . . . . 6 |- (y = (H` (F` B)) -> ((-. ((F |` suc B) = (/) \/ Lim dom ( F |` suc B)) /\ y = (H` ((F |` suc B)` U.dom ( F |` suc B)))) <-> (-. ((F |` suc B) = (/) \/ Lim dom ( F |` suc B)) /\ (H` (F` B)) = (H` ((F |` suc B)` U.dom ( F |` suc B))))))
37	19, 20, 34, 36	opelopab 2816	. . . . 5 |- (<.(F |` suc B), (H` (F` B))>. e. {<.x, y>. | (-. (x = (/) \/ Lim dom x) /\ y = (H` (x` U.dom x)))} <-> (-. ((F |` suc B) = (/) \/ Lim dom ( F |` suc B)) /\ (H` (F` B)) = (H` ((F |` suc B)` U.dom ( F |` suc B)))))
38		nsuceq0 3049	. . . . . . . 8 |- suc B =/= (/)
39		fndm 3583	. . . . . . . . . . . 12 |- (F Fn On -> dom F = On)
40	15, 39	ax-mp 7	. . . . . . . . . . 11 |- dom F = On
41	40	ineq2i 2211	. . . . . . . . . 10 |- (suc B i^i dom F) = (suc B i^i On)
42		dmres 3376	. . . . . . . . . 10 |- dom ( F |` suc B) = (suc B i^i dom F)
43	2	onss 3095	. . . . . . . . . . 11 |- suc B (_ On
44		dfss 2051	. . . . . . . . . . 11 |- (suc B (_ On <-> suc B = (suc B i^i On))
45	43, 44	mpbi 189	. . . . . . . . . 10 |- suc B = (suc B i^i On)
46	41, 42, 45	3eqtr4 1503	. . . . . . . . 9 |- dom ( F |` suc B) = suc B
47	46	eqeq1i 1480	. . . . . . . 8 |- (dom ( F |` suc B) = (/) <-> suc B = (/))
48	38, 47	nemtbir 1639	. . . . . . 7 |- -. dom ( F |` suc B) = (/)
49		dmeq 3307	. . . . . . . 8 |- ((F |` suc B) = (/) -> dom ( F |` suc B) = dom (/))
50		dm0 3319	. . . . . . . 8 |- dom (/) = (/)
51	49, 50	syl6eq 1521	. . . . . . 7 |- ((F |` suc B) = (/) -> dom ( F |` suc B) = (/))
52	48, 51	mto 106	. . . . . 6 |- -. (F |` suc B) = (/)
53	1	elisseti 1815	. . . . . . . 8 |- B e. V
54		nlimsucg 3108	. . . . . . . 8 |- (B e. V -> -. Lim suc B)
55	53, 54	ax-mp 7	. . . . . . 7 |- -. Lim suc B
56		limeq 2956	. . . . . . . 8 |- (dom ( F |` suc B) = suc B -> (Lim dom ( F |` suc B) <-> Lim suc B))
57	46, 56	ax-mp 7	. . . . . . 7 |- (Lim dom ( F |` suc B) <-> Lim suc B)
58	55, 57	mtbir 192	. . . . . 6 |- -. Lim dom ( F |` suc B)
59	52, 58	pm3.2ni 579	. . . . 5 |- -. ((F |` suc B) = (/) \/ Lim dom ( F |` suc B))
60	53	sucid 3047	. . . . . . . 8 |- B e. suc B
61		fvres 3729	. . . . . . . 8 |- (B e. suc B -> ((F |` suc B)` B) = (F` B))
62	60, 61	ax-mp 7	. . . . . . 7 |- ((F |` suc B)` B) = (F` B)
63	46	unieqi 2507	. . . . . . . . 9 |- U.dom ( F |` suc B) = U.suc B
64	1	onunisuc 3102	. . . . . . . . 9 |- U.suc B = B
65	63, 64	eqtr2 1494	. . . . . . . 8 |- B = U.dom ( F |` suc B)
66	65	fveq2i 3722	. . . . . . 7 |- ((F |` suc B)` B) = ((F |` suc B)` U.dom ( F |` suc B))
67	62, 66	eqtr3 1495	. . . . . 6 |- (F` B) = ((F |` suc B)` U.dom ( F |` suc B))
68	67	fveq2i 3722	. . . . 5 |- (H` (F` B)) = (H` ((F |` suc B)` U.dom ( F |` suc B)))
69	37, 59, 68	mpbir2an 729	. . . 4 |- <.(F |` suc B), (H` (F`