Theorem tz7.44-2

Description: The value of F at a successor ordinal. Part 2 of Theorem 7.44 of TakeutiZaring p. 49. (Contributed by NM, 23-Apr-1995) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012) (Revised by Mario Carneiro, 14-Nov-2014)

	Ref	Expression
Hypotheses	tz7.44.1	$$⊢G=\left(x\in \mathrm{V}⟼if\left(x=\varnothing ,A,if\left(\mathrm{Lim}\mathrm{dom}x,\bigcup \mathrm{ran}x,H\left(x\left(\bigcup \mathrm{dom}x\right)\right)\right)\right)\right)$$
	tz7.44.2	$$⊢y\in X\to F\left(y\right)=G\left({F\upharpoonright }_y\right)$$
	tz7.44.3	$$⊢y\in X\to {F\upharpoonright }_y\in \mathrm{V}$$
	tz7.44.4	$$⊢FFnX$$
	tz7.44.5	$$⊢\mathrm{Ord}X$$
Assertion	tz7.44-2	$$⊢\mathrm{suc}B\in X\to F\left(\mathrm{suc}B\right)=H\left(F\left(B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		tz7.44.1	$$⊢G=\left(x\in \mathrm{V}⟼if\left(x=\varnothing ,A,if\left(\mathrm{Lim}\mathrm{dom}x,\bigcup \mathrm{ran}x,H\left(x\left(\bigcup \mathrm{dom}x\right)\right)\right)\right)\right)$$
2		tz7.44.2	$$⊢y\in X\to F\left(y\right)=G\left({F\upharpoonright }_y\right)$$
3		tz7.44.3	$$⊢y\in X\to {F\upharpoonright }_y\in \mathrm{V}$$
4		tz7.44.4	$$⊢FFnX$$
5		tz7.44.5	$$⊢\mathrm{Ord}X$$
6		fveq2	$$⊢y=\mathrm{suc}B\to F\left(y\right)=F\left(\mathrm{suc}B\right)$$
7		reseq2	$$⊢y=\mathrm{suc}B\to {F\upharpoonright }_y={F\upharpoonright }_{\mathrm{suc}B}$$
8	7	fveq2d	$$⊢y=\mathrm{suc}B\to G\left({F\upharpoonright }_y\right)=G\left({F\upharpoonright }_{\mathrm{suc}B}\right)$$
9	6 8	eqeq12d	$$⊢y=\mathrm{suc}B\to \left(F\left(y\right)=G\left({F\upharpoonright }_y\right)\leftrightarrow F\left(\mathrm{suc}B\right)=G\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)$$
10	9 2	vtoclga	$$⊢\mathrm{suc}B\in X\to F\left(\mathrm{suc}B\right)=G\left({F\upharpoonright }_{\mathrm{suc}B}\right)$$
11		eqeq1	$$⊢x={F\upharpoonright }_{\mathrm{suc}B}\to \left(x=\varnothing \leftrightarrow {F\upharpoonright }_{\mathrm{suc}B}=\varnothing \right)$$
12		dmeq	$$⊢x={F\upharpoonright }_{\mathrm{suc}B}\to \mathrm{dom}x=\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)$$
13		limeq	$$⊢\mathrm{dom}x=\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\to \left(\mathrm{Lim}\mathrm{dom}x\leftrightarrow \mathrm{Lim}\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)$$
14	12 13	syl	$$⊢x={F\upharpoonright }_{\mathrm{suc}B}\to \left(\mathrm{Lim}\mathrm{dom}x\leftrightarrow \mathrm{Lim}\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)$$
15		rneq	$$⊢x={F\upharpoonright }_{\mathrm{suc}B}\to \mathrm{ran}x=\mathrm{ran}\left({F\upharpoonright }_{\mathrm{suc}B}\right)$$
16	15	unieqd	$$⊢x={F\upharpoonright }_{\mathrm{suc}B}\to \bigcup \mathrm{ran}x=\bigcup \mathrm{ran}\left({F\upharpoonright }_{\mathrm{suc}B}\right)$$
17		fveq1	$$⊢x={F\upharpoonright }_{\mathrm{suc}B}\to x\left(\bigcup \mathrm{dom}x\right)=\left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(\bigcup \mathrm{dom}x\right)$$
18	12	unieqd	$$⊢x={F\upharpoonright }_{\mathrm{suc}B}\to \bigcup \mathrm{dom}x=\bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)$$
19	18	fveq2d	$$⊢x={F\upharpoonright }_{\mathrm{suc}B}\to \left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(\bigcup \mathrm{dom}x\right)=\left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(\bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)$$
20	17 19	eqtrd	$$⊢x={F\upharpoonright }_{\mathrm{suc}B}\to x\left(\bigcup \mathrm{dom}x\right)=\left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(\bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)$$
21	20	fveq2d	$$⊢x={F\upharpoonright }_{\mathrm{suc}B}\to H\left(x\left(\bigcup \mathrm{dom}x\right)\right)=H\left(\left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(\bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)\right)$$
22	14 16 21	ifbieq12d	$$⊢x={F\upharpoonright }_{\mathrm{suc}B}\to if\left(\mathrm{Lim}\mathrm{dom}x,\bigcup \mathrm{ran}x,H\left(x\left(\bigcup \mathrm{dom}x\right)\right)\right)=if\left(\mathrm{Lim}\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right),\bigcup \mathrm{ran}\left({F\upharpoonright }_{\mathrm{suc}B}\right),H\left(\left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(\bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)\right)\right)$$
23	11 22	ifbieq2d	$$⊢x={F\upharpoonright }_{\mathrm{suc}B}\to if\left(x=\varnothing ,A,if\left(\mathrm{Lim}\mathrm{dom}x,\bigcup \mathrm{ran}x,H\left(x\left(\bigcup \mathrm{dom}x\right)\right)\right)\right)=if\left({F\upharpoonright }_{\mathrm{suc}B}=\varnothing ,A,if\left(\mathrm{Lim}\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right),\bigcup \mathrm{ran}\left({F\upharpoonright }_{\mathrm{suc}B}\right),H\left(\left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(\bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)\right)\right)\right)$$
24	7	eleq1d	$$⊢y=\mathrm{suc}B\to \left({F\upharpoonright }_y\in \mathrm{V}\leftrightarrow {F\upharpoonright }_{\mathrm{suc}B}\in \mathrm{V}\right)$$
25	24 3	vtoclga	$$⊢\mathrm{suc}B\in X\to {F\upharpoonright }_{\mathrm{suc}B}\in \mathrm{V}$$
26		noel	$$⊢\neg B\in \varnothing$$
27		dmeq	$$⊢{F\upharpoonright }_{\mathrm{suc}B}=\varnothing \to \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)=\mathrm{dom}\varnothing$$
28		dm0	$$⊢\mathrm{dom}\varnothing =\varnothing$$
29	27 28	eqtrdi	$$⊢{F\upharpoonright }_{\mathrm{suc}B}=\varnothing \to \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)=\varnothing$$
30		ordsson	$$⊢\mathrm{Ord}X\to X\subseteq \mathrm{On}$$
31	5 30	ax-mp	$$⊢X\subseteq \mathrm{On}$$
32		ordtr	$$⊢\mathrm{Ord}X\to \mathrm{Tr}X$$
33	5 32	ax-mp	$$⊢\mathrm{Tr}X$$
34		trsuc	$$⊢\left(\mathrm{Tr}X\wedge \mathrm{suc}B\in X\right)\to B\in X$$
35	33 34	mpan	$$⊢\mathrm{suc}B\in X\to B\in X$$
36	31 35	sseldi	$$⊢\mathrm{suc}B\in X\to B\in \mathrm{On}$$
37		sucidg	$$⊢B\in \mathrm{On}\to B\in \mathrm{suc}B$$
38	36 37	syl	$$⊢\mathrm{suc}B\in X\to B\in \mathrm{suc}B$$
39		dmres	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)=\mathrm{suc}B\cap \mathrm{dom}F$$
40		ordelss	$$⊢\left(\mathrm{Ord}X\wedge \mathrm{suc}B\in X\right)\to \mathrm{suc}B\subseteq X$$
41	5 40	mpan	$$⊢\mathrm{suc}B\in X\to \mathrm{suc}B\subseteq X$$
42	4	fndmi	$$⊢\mathrm{dom}F=X$$
43	41 42	sseqtrrdi	$$⊢\mathrm{suc}B\in X\to \mathrm{suc}B\subseteq \mathrm{dom}F$$
44		df-ss	$$⊢\mathrm{suc}B\subseteq \mathrm{dom}F\leftrightarrow \mathrm{suc}B\cap \mathrm{dom}F=\mathrm{suc}B$$
45	43 44	sylib	$$⊢\mathrm{suc}B\in X\to \mathrm{suc}B\cap \mathrm{dom}F=\mathrm{suc}B$$
46	39 45	syl5eq	$$⊢\mathrm{suc}B\in X\to \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)=\mathrm{suc}B$$
47	38 46	eleqtrrd	$$⊢\mathrm{suc}B\in X\to B\in \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)$$
48		eleq2	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)=\varnothing \to \left(B\in \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\leftrightarrow B\in \varnothing \right)$$
49	47 48	syl5ibcom	$$⊢\mathrm{suc}B\in X\to \left(\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)=\varnothing \to B\in \varnothing \right)$$
50	29 49	syl5	$$⊢\mathrm{suc}B\in X\to \left({F\upharpoonright }_{\mathrm{suc}B}=\varnothing \to B\in \varnothing \right)$$
51	26 50	mtoi	$$⊢\mathrm{suc}B\in X\to \neg {F\upharpoonright }_{\mathrm{suc}B}=\varnothing$$
52	51	iffalsed	$$⊢\mathrm{suc}B\in X\to if\left({F\upharpoonright }_{\mathrm{suc}B}=\varnothing ,A,if\left(\mathrm{Lim}\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right),\bigcup \mathrm{ran}\left({F\upharpoonright }_{\mathrm{suc}B}\right),H\left(\left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(\bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)\right)\right)\right)=if\left(\mathrm{Lim}\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right),\bigcup \mathrm{ran}\left({F\upharpoonright }_{\mathrm{suc}B}\right),H\left(\left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(\bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)\right)\right)$$
53		nlimsucg	$$⊢B\in \mathrm{On}\to \neg \mathrm{Lim}\mathrm{suc}B$$
54	36 53	syl	$$⊢\mathrm{suc}B\in X\to \neg \mathrm{Lim}\mathrm{suc}B$$
55		limeq	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)=\mathrm{suc}B\to \left(\mathrm{Lim}\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\leftrightarrow \mathrm{Lim}\mathrm{suc}B\right)$$
56	46 55	syl	$$⊢\mathrm{suc}B\in X\to \left(\mathrm{Lim}\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\leftrightarrow \mathrm{Lim}\mathrm{suc}B\right)$$
57	54 56	mtbird	$$⊢\mathrm{suc}B\in X\to \neg \mathrm{Lim}\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)$$
58	57	iffalsed	$$⊢\mathrm{suc}B\in X\to if\left(\mathrm{Lim}\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right),\bigcup \mathrm{ran}\left({F\upharpoonright }_{\mathrm{suc}B}\right),H\left(\left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(\bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)\right)\right)=H\left(\left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(\bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)\right)$$
59	46	unieqd	$$⊢\mathrm{suc}B\in X\to \bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)=\bigcup \mathrm{suc}B$$
60		eloni	$$⊢B\in \mathrm{On}\to \mathrm{Ord}B$$
61		ordunisuc	$$⊢\mathrm{Ord}B\to \bigcup \mathrm{suc}B=B$$
62	36 60 61	3syl	$$⊢\mathrm{suc}B\in X\to \bigcup \mathrm{suc}B=B$$
63	59 62	eqtrd	$$⊢\mathrm{suc}B\in X\to \bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)=B$$
64	63	fveq2d	$$⊢\mathrm{suc}B\in X\to \left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(\bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)=\left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(B\right)$$
65	38	fvresd	$$⊢\mathrm{suc}B\in X\to \left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(B\right)=F\left(B\right)$$
66	64 65	eqtrd	$$⊢\mathrm{suc}B\in X\to \left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(\bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)=F\left(B\right)$$
67	66	fveq2d	$$⊢\mathrm{suc}B\in X\to H\left(\left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(\bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)\right)=H\left(F\left(B\right)\right)$$
68	52 58 67	3eqtrd	$$⊢\mathrm{suc}B\in X\to if\left({F\upharpoonright }_{\mathrm{suc}B}=\varnothing ,A,if\left(\mathrm{Lim}\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right),\bigcup \mathrm{ran}\left({F\upharpoonright }_{\mathrm{suc}B}\right),H\left(\left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(\bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)\right)\right)\right)=H\left(F\left(B\right)\right)$$
69		fvex	$$⊢H\left(F\left(B\right)\right)\in \mathrm{V}$$
70	68 69	eqeltrdi	$$⊢\mathrm{suc}B\in X\to if\left({F\upharpoonright }_{\mathrm{suc}B}=\varnothing ,A,if\left(\mathrm{Lim}\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right),\bigcup \mathrm{ran}\left({F\upharpoonright }_{\mathrm{suc}B}\right),H\left(\left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(\bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)\right)\right)\right)\in \mathrm{V}$$
71	1 23 25 70	fvmptd3	$$⊢\mathrm{suc}B\in X\to G\left({F\upharpoonright }_{\mathrm{suc}B}\right)=if\left({F\upharpoonright }_{\mathrm{suc}B}=\varnothing ,A,if\left(\mathrm{Lim}\mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right),\bigcup \mathrm{ran}\left({F\upharpoonright }_{\mathrm{suc}B}\right),H\left(\left({F\upharpoonright }_{\mathrm{suc}B}\right)\left(\bigcup \mathrm{dom}\left({F\upharpoonright }_{\mathrm{suc}B}\right)\right)\right)\right)\right)$$
72	10 71 68	3eqtrd	$$⊢\mathrm{suc}B\in X\to F\left(\mathrm{suc}B\right)=H\left(F\left(B\right)\right)$$