Theorem tz7.44-2 3914

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 3095	. . 3 |- suc B e. On
3		fveq2 3709	. . . . 5 |- (x = suc B -> (F` x) = (F` suc B))
4		reseq2 3353	. . . . . 6 |- (x = suc B -> (F |` x) = (F |` suc B))
5	4	fveq2d 3713	. . . . 5 |- (x = suc B -> (G` (F |` x)) = (G` (F |` suc B)))
6	3, 5	eqeq12d 1481	. . . 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 1843	. . 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 3912	. . 3 |- Fun G
12		3mix2 814	. . . . . 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 2812	. . . . 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 2084	. . . 4 |- {<.x, y>. | (-. (x = (/) \/ Lim dom x) /\ y = (H` (x` U.dom x)))} (_ G
15		tz7.44.2	. . . . . . . 8 |- F Fn On
16		fnfun 3571	. . . . . . . 8 |- (F Fn On -> Fun F)
17	15, 16	ax-mp 7	. . . . . . 7 |- Fun F
18		resfunexg 3565	. . . . . . 7 |- ((Fun F /\ suc B e. On) -> (F |` suc B) e. V)
19	17, 2, 18	mp2an 695	. . . . . 6 |- (F |` suc B) e. V
20		fvex 3717	. . . . . 6 |- (H` (F` B)) e. V
21		eqeq1 1473	. . . . . . . . 9 |- (x = (F |` suc B) -> (x = (/) <-> (F |` suc B) = (/)))
22		dmeq 3300	. . . . . . . . . 10 |- (x = (F |` suc B) -> dom x = dom ( F |` suc B))
23		limeq 2950	. . . . . . . . . 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 625	. . . . . . . 8 |- (x = (F |` suc B) -> ((x = (/) \/ Lim dom x) <-> ((F |` suc B) = (/) \/ Lim dom ( F |` suc B))))
26	25	negbid 609	. . . . . . 7 |- (x = (F |` suc B) -> (-. (x = (/) \/ Lim dom x) <-> -. ((F |` suc B) = (/) \/ Lim dom ( F |` suc B))))
27		unieq 2500	. . . . . . . . . . 11 |- (dom x = dom ( F |` suc B) -> U.dom x = U.dom ( F |` suc B))
28		fveq2 3709	. . . . . . . . . . 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 3708	. . . . . . . . . 10 |- (x = (F |` suc B) -> (x` U.dom ( F |` suc B)) = ((F |` suc B)` U.dom ( F |` suc B)))
31	29, 30	eqtrd 1499	. . . . . . . . 9 |- (x = (F |` suc B) -> (x` U.dom x) = ((F |` suc B)` U.dom ( F |` suc B)))
32	31	fveq2d 3713	. . . . . . . 8 |- (x = (F |` suc B) -> (H` (x` U.dom x)) = (H` ((F |` suc B)` U.dom ( F |` suc B))))
33	32	eqeq2d 1478	. . . . . . 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 626	. . . . . 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 1473	. . . . . . 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 614	. . . . . 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 2809	. . . . 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 3043	. . . . . . . 8 |- suc B =/= (/)
39		fndm 3573	. . . . . . . . . . . 12 |- (F Fn On -> dom F = On)
40	15, 39	ax-mp 7	. . . . . . . . . . 11 |- dom F = On
41	40	ineq2i 2204	. . . . . . . . . 10 |- (suc B i^i dom F) = (suc B i^i On)
42		dmres 3364	. . . . . . . . . 10 |- dom ( F |` suc B) = (suc B i^i dom F)
43	2	onss 3089	. . . . . . . . . . 11 |- suc B (_ On
44		dfss 2044	. . . . . . . . . . 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 1497	. . . . . . . . 9 |- dom ( F |` suc B) = suc B
47	46	eqeq1i 1474	. . . . . . . 8 |- (dom ( F |` suc B) = (/) <-> suc B = (/))
48	38, 47	nemtbir 1633	. . . . . . 7 |- -. dom ( F |` suc B) = (/)
49		dmeq 3300	. . . . . . . 8 |- ((F |` suc B) = (/) -> dom ( F |` suc B) = dom (/))
50		dm0 3312	. . . . . . . 8 |- dom (/) = (/)
51	49, 50	syl6eq 1515	. . . . . . 7 |- ((F |` suc B) = (/) -> dom ( F |` suc B) = (/))
52	48, 51	mto 106	. . . . . 6 |- -. (F |` suc B) = (/)
53	1	elisseti 1809	. . . . . . . 8 |- B e. V
54		nlimsucg 3102	. . . . . . . 8 |- (B e. V -> -. Lim suc B)
55	53, 54	ax-mp 7	. . . . . . 7 |- -. Lim suc B
56		limeq 2950	. . . . . . . 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 578	. . . . 5 |- -. ((F |` suc B) = (/) \/ Lim dom ( F |` suc B))
60	53	sucid 3041	. . . . . . . 8 |- B e. suc B
61		fvres 3719	. . . . . . . 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 2501	. . . . . . . . 9 |- U.dom ( F |` suc B) = U.suc B
64	1	onunisuc 3096	. . . . . . . . 9 |- U.suc B = B
65	63, 64	eqtr2 1488	. . . . . . . 8 |- B = U.dom ( F |` suc B)
66	65	fveq2i 3712	. . . . . . 7 |- ((F |` suc B)` B) = ((F |` suc B)` U.dom ( F |` suc B))
67	62, 66	eqtr3 1489	. . . . . 6 |- (F` B) = ((F |` suc B)` U.dom ( F |` suc B))
68	67	fveq2i 3712	. . . . 5 |- (H` (F` B)) = (H` ((F |` suc B)` U.dom ( F |` suc B)))
69	37, 59, 68	mpbir2an 728	. . . 4 |- <.(F |` suc B), (H` (F`