Theorem tz7.44-2 2967

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 group(s):   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 2353	. . 3 |- suc B e. On
3		fveq2 2832	. . . . 5 |- (x = suc B -> (F` x) = (F` suc B))
4		reseq2 2576	. . . . . 6 |- (x = suc B -> (F |` x) = (F |` suc B))
5	4	fveq2d 2836	. . . . 5 |- (x = suc B -> (G` (F |` x)) = (G` (F |` suc B)))
6	3, 5	cleq12d 1115	. . . 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 1387	. . 3 |- (suc B e. On -> (F` suc B) = (G` (F |` suc B)))
9	2, 8	ax-mp 6	. 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 2965	. . 3 |- Fun G
12		3mix2 601	. . . . . 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 2120	. . . . 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 1533	. . . 4 |- {<.x, y>. | (-. (x = (/) \/ Lim dom x) /\ y = (H` (x` U.dom x)))} (_ G
15		nsuceq0 2306	. . . . . . . . 9 |- -. suc B = (/)
16		tz7.44.2	. . . . . . . . . . . . 13 |- F Fn On
17		fndm 2723	. . . . . . . . . . . . 13 |- (F Fn On -> dom F = On)
18	16, 17	ax-mp 6	. . . . . . . . . . . 12 |- dom F = On
19	18	ineq2i 1642	. . . . . . . . . . 11 |- (suc B i^i dom F) = (suc B i^i On)
20		dmres 2584	. . . . . . . . . . 11 |- dom (F |` suc B) = (suc B i^i dom F)
21	2	onss 2347	. . . . . . . . . . . 12 |- suc B (_ On
22		dfss 1493	. . . . . . . . . . . 12 |- (suc B (_ On <-> suc B = (suc B i^i On))
23	21, 22	mpbi 164	. . . . . . . . . . 11 |- suc B = (suc B i^i On)
24	19, 20, 23	3eqtr4 1126	. . . . . . . . . 10 |- dom (F |` suc B) = suc B
25	24	cleq1i 1108	. . . . . . . . 9 |- (dom (F |` suc B) = (/) <-> suc B = (/))
26	15, 25	mtbir 167	. . . . . . . 8 |- -. dom (F |` suc B) = (/)
27		dmeq 2531	. . . . . . . . 9 |- ((F |` suc B) = (/) -> dom (F |` suc B) = dom (/))
28		dm0 2542	. . . . . . . . 9 |- dom (/) = (/)
29	27, 28	syl6eq 1140	. . . . . . . 8 |- ((F |` suc B) = (/) -> dom (F |` suc B) = (/))
30	26, 29	mto 93	. . . . . . 7 |- -. (F |` suc B) = (/)
31	1	elisseti 1355	. . . . . . . . 9 |- B e. V
32	31	nlimsuc 2363	. . . . . . . 8 |- -. Lim suc B
33		limeq 2211	. . . . . . . . 9 |- (dom (F |` suc B) = suc B -> (Lim dom (F |` suc B) <-> Lim suc B))
34	24, 33	ax-mp 6	. . . . . . . 8 |- (Lim dom (F |` suc B) <-> Lim suc B)
35	32, 34	mtbir 167	. . . . . . 7 |- -. Lim dom (F |` suc B)
36	30, 35	pm3.2ni 440	. . . . . 6 |- -. ((F |` suc B) = (/) \/ Lim dom (F |` suc B))
37	31	sucid 2304	. . . . . . . . 9 |- B e. suc B
38		fvres 2840	. . . . . . . . 9 |- (B e. suc B -> ((F |` suc B)` B) = (F` B))
39	37, 38	ax-mp 6	. . . . . . . 8 |- ((F |` suc B)` B) = (F` B)
40	24	unieqi 1928	. . . . . . . . . 10 |- U.dom (F |` suc B) = U.suc B
41	1	onunisuc 2354	. . . . . . . . . 10 |- U.suc B = B
42	40, 41	eqtr2 1120	. . . . . . . . 9 |- B = U.dom (F |` suc B)
43	42	fveq2i 2835	. . . . . . . 8 |- ((F |` suc B)` B) = ((F |` suc B)` U.dom (F |` suc B))
44	39, 43	eqtr3 1121	. . . . . . 7 |- (F` B) = ((F |` suc B)` U.dom (F |` suc B))
45	44	fveq2i 2835	. . . . . 6 |- (H` (F` B)) = (H` ((F |` suc B)` U.dom (F |` suc B)))
46	36, 45	pm3.2i 234	. . . . 5 |- (-. ((F |` suc B) = (/) \/ Lim dom (F |` suc B)) /\ (H` (F` B)) = (H` ((F |` suc B)` U.dom (F |` suc B))))
47		fnfun 2721	. . . . . . . 8 |- (F Fn On -> Fun F)
48	16, 47	ax-mp 6	. . . . . . 7 |- Fun F
49		resfunexg 2717	. . . . . . 7 |- (suc B e. On -> (Fun F -> (F |` suc B) e. V))
50	2, 48, 49	mp2 43	. . . . . 6 |- (F |` suc B) e. V
51		fvex 2838	. . . . . 6 |- (H` (F` B)) e. V
52		cleq1 1107	. . . . . . . . 9 |- (x = (F |` suc B) -> (x = (/) <-> (F |` suc B) = (/)))
53		dmeq 2531	. . . . . . . . . 10 |- (x = (F |` suc B) -> dom x = dom (F |` suc B))
54		limeq 2211	. . . . . . . . . 10 |- (dom x = dom (F |` suc B) -> (Lim dom x <-> Lim dom (F |` suc B)))
55	53, 54	syl 12	. . . . . . . . 9 |- (x = (F |` suc B) -> (Lim dom x <-> Lim dom (F |` suc B)))
56	52, 55	orbi12d 475	. . . . . . . 8 |- (x = (F |` suc B) -> ((x = (/) \/ Lim dom x) <-> ((F |` suc B) = (/) \/ Lim dom (F |` suc B))))
57	56	negbid 463	. . . . . . 7 |- (x = (F |` suc B) -> (-. (x = (/) \/ Lim dom x) <-> -. ((F |` suc B) = (/) \/ Lim dom (F |` suc B))))
58		unieq 1927	. . . . . . . . . . 11 |- (dom x = dom (F |` suc B) -> U.dom x = U.dom (F |` suc B))
59		fveq2 2832	. . . . . . . . . . 11 |- (U.dom x = U.dom (F |` suc B) -> (x` U.dom x) = (x` U.dom (F |` suc B)))
60	53, 58, 59	3syl 21	. . . . . . . . . 10 |- (x = (F |` suc B) -> (x` U.dom x) = (x` U.dom (F |` suc B)))
61		fveq1 2831	. . . . . . . . . 10 |- (x = (F |` suc B) -> (x` U.dom (F |` suc B)) = ((F |` suc B)` U.dom (F |` suc B)))
62	60, 61	eqtrd 1128	. . . . . . . . 9 |- (x = (F |` suc B) -> (x` U.dom x) = ((F |` suc B)` U.dom (F |` suc B)))
63	62	fveq2d 2836	. . . . . . . 8 |- (x = (F |` suc B) -> (H` (x` U.dom x)) = (H` ((F |` suc B)` U.dom (F |` suc B))))
64	63	cleq2d 1112	. . . . . . 7 |- (x = (F |` suc B) -> (y = (H` (x` U.dom x)) <-> y = (H` ((F |` suc B)` U.dom (F |` suc B)))))
65	57, 64	anbi12d 476	. . . . . 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))))))
66		cleq1 1107	. . . . . . 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)))))
67	66	anbi2d 468	. . . . . 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))))))
68	50, 51, 65, 67	opelopab 2117	. . . . 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)))))
69	46, 68	mpbir 165	. . . 4 |- <.(F |` suc B), (H` (F` B))>. e. {<.x, y>. | (-. (x = (/) \/ Lim dom x)