Theorem dfrdg2

Description: Alternate definition of the recursive function generator when I is a set. (Contributed by Scott Fenton, 26-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	dfrdg2	$$⊢I\in V\to \mathrm{rec}\left(F,I\right)=\bigcup \left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=if\left(y=\varnothing ,I,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		rdgeq2	$$⊢i=I\to \mathrm{rec}\left(F,i\right)=\mathrm{rec}\left(F,I\right)$$
2		ifeq1	$$⊢i=I\to if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)=if\left(y=\varnothing ,I,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)$$
3	2	eqeq2d	$$⊢i=I\to \left(f\left(y\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\leftrightarrow f\left(y\right)=if\left(y=\varnothing ,I,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)$$
4	3	ralbidv	$$⊢i=I\to \left(\forall y\in xf\left(y\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\leftrightarrow \forall y\in xf\left(y\right)=if\left(y=\varnothing ,I,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)$$
5	4	anbi2d	$$⊢i=I\to \left(\left(fFnx\wedge \forall y\in xf\left(y\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)\leftrightarrow \left(fFnx\wedge \forall y\in xf\left(y\right)=if\left(y=\varnothing ,I,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)\right)$$
6	5	rexbidv	$$⊢i=I\to \left(\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)\leftrightarrow \exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=if\left(y=\varnothing ,I,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)\right)$$
7	6	abbidv	$$⊢i=I\to \left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)\right\}=\left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=if\left(y=\varnothing ,I,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)\right\}$$
8	7	unieqd	$$⊢i=I\to \bigcup \left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)\right\}=\bigcup \left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=if\left(y=\varnothing ,I,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)\right\}$$
9	1 8	eqeq12d	$$⊢i=I\to \left(\mathrm{rec}\left(F,i\right)=\bigcup \left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)\right\}\leftrightarrow \mathrm{rec}\left(F,I\right)=\bigcup \left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=if\left(y=\varnothing ,I,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)\right\}\right)$$
10		df-rdg	$$⊢\mathrm{rec}\left(F,i\right)=\mathrm{recs}\left(\left(g\in \mathrm{V}⟼if\left(g=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)\right)$$
11		dfrecs3	$$⊢\mathrm{recs}\left(\left(g\in \mathrm{V}⟼if\left(g=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)\right)=\bigcup \left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=\left(g\in \mathrm{V}⟼if\left(g=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)\left({f\upharpoonright }_y\right)\right)\right\}$$
12		vex	$$⊢f\in \mathrm{V}$$
13	12	resex	$$⊢{f\upharpoonright }_y\in \mathrm{V}$$
14		eqeq1	$$⊢g={f\upharpoonright }_y\to \left(g=\varnothing \leftrightarrow {f\upharpoonright }_y=\varnothing \right)$$
15		relres	$$⊢\mathrm{Rel}\left({f\upharpoonright }_y\right)$$
16		reldm0	$$⊢\mathrm{Rel}\left({f\upharpoonright }_y\right)\to \left({f\upharpoonright }_y=\varnothing \leftrightarrow \mathrm{dom}\left({f\upharpoonright }_y\right)=\varnothing \right)$$
17	15 16	ax-mp	$$⊢{f\upharpoonright }_y=\varnothing \leftrightarrow \mathrm{dom}\left({f\upharpoonright }_y\right)=\varnothing$$
18	14 17	bitrdi	$$⊢g={f\upharpoonright }_y\to \left(g=\varnothing \leftrightarrow \mathrm{dom}\left({f\upharpoonright }_y\right)=\varnothing \right)$$
19		dmeq	$$⊢g={f\upharpoonright }_y\to \mathrm{dom}g=\mathrm{dom}\left({f\upharpoonright }_y\right)$$
20		limeq	$$⊢\mathrm{dom}g=\mathrm{dom}\left({f\upharpoonright }_y\right)\to \left(\mathrm{Lim}\mathrm{dom}g\leftrightarrow \mathrm{Lim}\mathrm{dom}\left({f\upharpoonright }_y\right)\right)$$
21	19 20	syl	$$⊢g={f\upharpoonright }_y\to \left(\mathrm{Lim}\mathrm{dom}g\leftrightarrow \mathrm{Lim}\mathrm{dom}\left({f\upharpoonright }_y\right)\right)$$
22		rneq	$$⊢g={f\upharpoonright }_y\to \mathrm{ran}g=\mathrm{ran}\left({f\upharpoonright }_y\right)$$
23		df-ima	$$⊢f\left[y\right]=\mathrm{ran}\left({f\upharpoonright }_y\right)$$
24	22 23	eqtr4di	$$⊢g={f\upharpoonright }_y\to \mathrm{ran}g=f\left[y\right]$$
25	24	unieqd	$$⊢g={f\upharpoonright }_y\to \bigcup \mathrm{ran}g=\bigcup f\left[y\right]$$
26		id	$$⊢g={f\upharpoonright }_y\to g={f\upharpoonright }_y$$
27	19	unieqd	$$⊢g={f\upharpoonright }_y\to \bigcup \mathrm{dom}g=\bigcup \mathrm{dom}\left({f\upharpoonright }_y\right)$$
28	26 27	fveq12d	$$⊢g={f\upharpoonright }_y\to g\left(\bigcup \mathrm{dom}g\right)=\left({f\upharpoonright }_y\right)\left(\bigcup \mathrm{dom}\left({f\upharpoonright }_y\right)\right)$$
29	28	fveq2d	$$⊢g={f\upharpoonright }_y\to F\left(g\left(\bigcup \mathrm{dom}g\right)\right)=F\left(\left({f\upharpoonright }_y\right)\left(\bigcup \mathrm{dom}\left({f\upharpoonright }_y\right)\right)\right)$$
30	21 25 29	ifbieq12d	$$⊢g={f\upharpoonright }_y\to if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)=if\left(\mathrm{Lim}\mathrm{dom}\left({f\upharpoonright }_y\right),\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup \mathrm{dom}\left({f\upharpoonright }_y\right)\right)\right)\right)$$
31	18 30	ifbieq2d	$$⊢g={f\upharpoonright }_y\to if\left(g=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)=if\left(\mathrm{dom}\left({f\upharpoonright }_y\right)=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}\left({f\upharpoonright }_y\right),\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup \mathrm{dom}\left({f\upharpoonright }_y\right)\right)\right)\right)\right)$$
32		eqid	$$⊢\left(g\in \mathrm{V}⟼if\left(g=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)=\left(g\in \mathrm{V}⟼if\left(g=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)$$
33		vex	$$⊢i\in \mathrm{V}$$
34		imaexg	$$⊢f\in \mathrm{V}\to f\left[y\right]\in \mathrm{V}$$
35	12 34	ax-mp	$$⊢f\left[y\right]\in \mathrm{V}$$
36	35	uniex	$$⊢\bigcup f\left[y\right]\in \mathrm{V}$$
37		fvex	$$⊢F\left(\left({f\upharpoonright }_y\right)\left(\bigcup \mathrm{dom}\left({f\upharpoonright }_y\right)\right)\right)\in \mathrm{V}$$
38	36 37	ifex	$$⊢if\left(\mathrm{Lim}\mathrm{dom}\left({f\upharpoonright }_y\right),\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup \mathrm{dom}\left({f\upharpoonright }_y\right)\right)\right)\right)\in \mathrm{V}$$
39	33 38	ifex	$$⊢if\left(\mathrm{dom}\left({f\upharpoonright }_y\right)=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}\left({f\upharpoonright }_y\right),\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup \mathrm{dom}\left({f\upharpoonright }_y\right)\right)\right)\right)\right)\in \mathrm{V}$$
40	31 32 39	fvmpt	$$⊢{f\upharpoonright }_y\in \mathrm{V}\to \left(g\in \mathrm{V}⟼if\left(g=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)\left({f\upharpoonright }_y\right)=if\left(\mathrm{dom}\left({f\upharpoonright }_y\right)=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}\left({f\upharpoonright }_y\right),\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup \mathrm{dom}\left({f\upharpoonright }_y\right)\right)\right)\right)\right)$$
41	13 40	ax-mp	$$⊢\left(g\in \mathrm{V}⟼if\left(g=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)\left({f\upharpoonright }_y\right)=if\left(\mathrm{dom}\left({f\upharpoonright }_y\right)=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}\left({f\upharpoonright }_y\right),\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup \mathrm{dom}\left({f\upharpoonright }_y\right)\right)\right)\right)\right)$$
42		dmres	$$⊢\mathrm{dom}\left({f\upharpoonright }_y\right)=y\cap \mathrm{dom}f$$
43		onelss	$$⊢x\in \mathrm{On}\to \left(y\in x\to y\subseteq x\right)$$
44	43	imp	$$⊢\left(x\in \mathrm{On}\wedge y\in x\right)\to y\subseteq x$$
45	44	3adant2	$$⊢\left(x\in \mathrm{On}\wedge fFnx\wedge y\in x\right)\to y\subseteq x$$
46		fndm	$$⊢fFnx\to \mathrm{dom}f=x$$
47	46	3ad2ant2	$$⊢\left(x\in \mathrm{On}\wedge fFnx\wedge y\in x\right)\to \mathrm{dom}f=x$$
48	45 47	sseqtrrd	$$⊢\left(x\in \mathrm{On}\wedge fFnx\wedge y\in x\right)\to y\subseteq \mathrm{dom}f$$
49		dfss2	$$⊢y\subseteq \mathrm{dom}f\leftrightarrow y\cap \mathrm{dom}f=y$$
50	48 49	sylib	$$⊢\left(x\in \mathrm{On}\wedge fFnx\wedge y\in x\right)\to y\cap \mathrm{dom}f=y$$
51	42 50	eqtrid	$$⊢\left(x\in \mathrm{On}\wedge fFnx\wedge y\in x\right)\to \mathrm{dom}\left({f\upharpoonright }_y\right)=y$$
52		eqeq1	$$⊢\mathrm{dom}\left({f\upharpoonright }_y\right)=y\to \left(\mathrm{dom}\left({f\upharpoonright }_y\right)=\varnothing \leftrightarrow y=\varnothing \right)$$
53		limeq	$$⊢\mathrm{dom}\left({f\upharpoonright }_y\right)=y\to \left(\mathrm{Lim}\mathrm{dom}\left({f\upharpoonright }_y\right)\leftrightarrow \mathrm{Lim}y\right)$$
54		unieq	$$⊢\mathrm{dom}\left({f\upharpoonright }_y\right)=y\to \bigcup \mathrm{dom}\left({f\upharpoonright }_y\right)=\bigcup y$$
55	54	fveq2d	$$⊢\mathrm{dom}\left({f\upharpoonright }_y\right)=y\to \left({f\upharpoonright }_y\right)\left(\bigcup \mathrm{dom}\left({f\upharpoonright }_y\right)\right)=\left({f\upharpoonright }_y\right)\left(\bigcup y\right)$$
56	55	fveq2d	$$⊢\mathrm{dom}\left({f\upharpoonright }_y\right)=y\to F\left(\left({f\upharpoonright }_y\right)\left(\bigcup \mathrm{dom}\left({f\upharpoonright }_y\right)\right)\right)=F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)$$
57	53 56	ifbieq2d	$$⊢\mathrm{dom}\left({f\upharpoonright }_y\right)=y\to if\left(\mathrm{Lim}\mathrm{dom}\left({f\upharpoonright }_y\right),\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup \mathrm{dom}\left({f\upharpoonright }_y\right)\right)\right)\right)=if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)\right)$$
58	52 57	ifbieq2d	$$⊢\mathrm{dom}\left({f\upharpoonright }_y\right)=y\to if\left(\mathrm{dom}\left({f\upharpoonright }_y\right)=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}\left({f\upharpoonright }_y\right),\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup \mathrm{dom}\left({f\upharpoonright }_y\right)\right)\right)\right)\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)\right)\right)$$
59		onelon	$$⊢\left(x\in \mathrm{On}\wedge y\in x\right)\to y\in \mathrm{On}$$
60		eloni	$$⊢y\in \mathrm{On}\to \mathrm{Ord}y$$
61	59 60	syl	$$⊢\left(x\in \mathrm{On}\wedge y\in x\right)\to \mathrm{Ord}y$$
62	61	3adant2	$$⊢\left(x\in \mathrm{On}\wedge fFnx\wedge y\in x\right)\to \mathrm{Ord}y$$
63		ordzsl	$$⊢\mathrm{Ord}y\leftrightarrow \left(y=\varnothing \vee \exists z\in \mathrm{On}y=\mathrm{suc}z\vee \mathrm{Lim}y\right)$$
64		iftrue	$$⊢y=\varnothing \to if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)\right)\right)=i$$
65		iftrue	$$⊢y=\varnothing \to if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)=i$$
66	64 65	eqtr4d	$$⊢y=\varnothing \to if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)\right)\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)$$
67		vex	$$⊢z\in \mathrm{V}$$
68	67	sucid	$$⊢z\in \mathrm{suc}z$$
69		fvres	$$⊢z\in \mathrm{suc}z\to \left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(z\right)=f\left(z\right)$$
70	68 69	ax-mp	$$⊢\left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(z\right)=f\left(z\right)$$
71		eloni	$$⊢z\in \mathrm{On}\to \mathrm{Ord}z$$
72		ordunisuc	$$⊢\mathrm{Ord}z\to \bigcup \mathrm{suc}z=z$$
73	71 72	syl	$$⊢z\in \mathrm{On}\to \bigcup \mathrm{suc}z=z$$
74	73	fveq2d	$$⊢z\in \mathrm{On}\to \left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(\bigcup \mathrm{suc}z\right)=\left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(z\right)$$
75	73	fveq2d	$$⊢z\in \mathrm{On}\to f\left(\bigcup \mathrm{suc}z\right)=f\left(z\right)$$
76	70 74 75	3eqtr4a	$$⊢z\in \mathrm{On}\to \left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(\bigcup \mathrm{suc}z\right)=f\left(\bigcup \mathrm{suc}z\right)$$
77	76	fveq2d	$$⊢z\in \mathrm{On}\to F\left(\left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(\bigcup \mathrm{suc}z\right)\right)=F\left(f\left(\bigcup \mathrm{suc}z\right)\right)$$
78		nsuceq0	$$⊢\mathrm{suc}z\ne \varnothing$$
79	78	neii	$$⊢\neg \mathrm{suc}z=\varnothing$$
80	79	iffalsei	$$⊢if\left(\mathrm{suc}z=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(\bigcup \mathrm{suc}z\right)\right)\right)\right)=if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(\bigcup \mathrm{suc}z\right)\right)\right)$$
81		nlimsucg	$$⊢z\in \mathrm{V}\to \neg \mathrm{Lim}\mathrm{suc}z$$
82		iffalse	$$⊢\neg \mathrm{Lim}\mathrm{suc}z\to if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(\bigcup \mathrm{suc}z\right)\right)\right)=F\left(\left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(\bigcup \mathrm{suc}z\right)\right)$$
83	67 81 82	mp2b	$$⊢if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(\bigcup \mathrm{suc}z\right)\right)\right)=F\left(\left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(\bigcup \mathrm{suc}z\right)\right)$$
84	80 83	eqtri	$$⊢if\left(\mathrm{suc}z=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(\bigcup \mathrm{suc}z\right)\right)\right)\right)=F\left(\left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(\bigcup \mathrm{suc}z\right)\right)$$
85	79	iffalsei	$$⊢if\left(\mathrm{suc}z=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(f\left(\bigcup \mathrm{suc}z\right)\right)\right)\right)=if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(f\left(\bigcup \mathrm{suc}z\right)\right)\right)$$
86		iffalse	$$⊢\neg \mathrm{Lim}\mathrm{suc}z\to if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(f\left(\bigcup \mathrm{suc}z\right)\right)\right)=F\left(f\left(\bigcup \mathrm{suc}z\right)\right)$$
87	67 81 86	mp2b	$$⊢if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(f\left(\bigcup \mathrm{suc}z\right)\right)\right)=F\left(f\left(\bigcup \mathrm{suc}z\right)\right)$$
88	85 87	eqtri	$$⊢if\left(\mathrm{suc}z=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(f\left(\bigcup \mathrm{suc}z\right)\right)\right)\right)=F\left(f\left(\bigcup \mathrm{suc}z\right)\right)$$
89	77 84 88	3eqtr4g	$$⊢z\in \mathrm{On}\to if\left(\mathrm{suc}z=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(\bigcup \mathrm{suc}z\right)\right)\right)\right)=if\left(\mathrm{suc}z=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(f\left(\bigcup \mathrm{suc}z\right)\right)\right)\right)$$
90		eqeq1	$$⊢y=\mathrm{suc}z\to \left(y=\varnothing \leftrightarrow \mathrm{suc}z=\varnothing \right)$$
91		limeq	$$⊢y=\mathrm{suc}z\to \left(\mathrm{Lim}y\leftrightarrow \mathrm{Lim}\mathrm{suc}z\right)$$
92		reseq2	$$⊢y=\mathrm{suc}z\to {f\upharpoonright }_y={f\upharpoonright }_{\mathrm{suc}z}$$
93		unieq	$$⊢y=\mathrm{suc}z\to \bigcup y=\bigcup \mathrm{suc}z$$
94	92 93	fveq12d	$$⊢y=\mathrm{suc}z\to \left({f\upharpoonright }_y\right)\left(\bigcup y\right)=\left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(\bigcup \mathrm{suc}z\right)$$
95	94	fveq2d	$$⊢y=\mathrm{suc}z\to F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)=F\left(\left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(\bigcup \mathrm{suc}z\right)\right)$$
96	91 95	ifbieq2d	$$⊢y=\mathrm{suc}z\to if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)\right)=if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(\bigcup \mathrm{suc}z\right)\right)\right)$$
97	90 96	ifbieq2d	$$⊢y=\mathrm{suc}z\to if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)\right)\right)=if\left(\mathrm{suc}z=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(\bigcup \mathrm{suc}z\right)\right)\right)\right)$$
98	93	fveq2d	$$⊢y=\mathrm{suc}z\to f\left(\bigcup y\right)=f\left(\bigcup \mathrm{suc}z\right)$$
99	98	fveq2d	$$⊢y=\mathrm{suc}z\to F\left(f\left(\bigcup y\right)\right)=F\left(f\left(\bigcup \mathrm{suc}z\right)\right)$$
100	91 99	ifbieq2d	$$⊢y=\mathrm{suc}z\to if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)=if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(f\left(\bigcup \mathrm{suc}z\right)\right)\right)$$
101	90 100	ifbieq2d	$$⊢y=\mathrm{suc}z\to if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)=if\left(\mathrm{suc}z=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(f\left(\bigcup \mathrm{suc}z\right)\right)\right)\right)$$
102	97 101	eqeq12d	$$⊢y=\mathrm{suc}z\to \left(if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)\right)\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\leftrightarrow if\left(\mathrm{suc}z=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_{\mathrm{suc}z}\right)\left(\bigcup \mathrm{suc}z\right)\right)\right)\right)=if\left(\mathrm{suc}z=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{suc}z,\bigcup f\left[y\right],F\left(f\left(\bigcup \mathrm{suc}z\right)\right)\right)\right)\right)$$
103	89 102	syl5ibrcom	$$⊢z\in \mathrm{On}\to \left(y=\mathrm{suc}z\to if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)\right)\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)$$
104	103	rexlimiv	$$⊢\exists z\in \mathrm{On}y=\mathrm{suc}z\to if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)\right)\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)$$
105		iftrue	$$⊢\mathrm{Lim}y\to if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)\right)=\bigcup f\left[y\right]$$
106		df-lim	$$⊢\mathrm{Lim}y\leftrightarrow \left(\mathrm{Ord}y\wedge y\ne \varnothing \wedge y=\bigcup y\right)$$
107	106	simp2bi	$$⊢\mathrm{Lim}y\to y\ne \varnothing$$
108	107	neneqd	$$⊢\mathrm{Lim}y\to \neg y=\varnothing$$
109	108	iffalsed	$$⊢\mathrm{Lim}y\to if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)\right)\right)=if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)\right)$$
110		iftrue	$$⊢\mathrm{Lim}y\to if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)=\bigcup f\left[y\right]$$
111	105 109 110	3eqtr4d	$$⊢\mathrm{Lim}y\to if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)\right)\right)=if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)$$
112	108	iffalsed	$$⊢\mathrm{Lim}y\to if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)=if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)$$
113	111 112	eqtr4d	$$⊢\mathrm{Lim}y\to if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)\right)\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)$$
114	66 104 113	3jaoi	$$⊢\left(y=\varnothing \vee \exists z\in \mathrm{On}y=\mathrm{suc}z\vee \mathrm{Lim}y\right)\to if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)\right)\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)$$
115	63 114	sylbi	$$⊢\mathrm{Ord}y\to if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)\right)\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)$$
116	62 115	syl	$$⊢\left(x\in \mathrm{On}\wedge fFnx\wedge y\in x\right)\to if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup y\right)\right)\right)\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)$$
117	58 116	sylan9eqr	$$⊢\left(\left(x\in \mathrm{On}\wedge fFnx\wedge y\in x\right)\wedge \mathrm{dom}\left({f\upharpoonright }_y\right)=y\right)\to if\left(\mathrm{dom}\left({f\upharpoonright }_y\right)=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}\left({f\upharpoonright }_y\right),\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup \mathrm{dom}\left({f\upharpoonright }_y\right)\right)\right)\right)\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)$$
118	51 117	mpdan	$$⊢\left(x\in \mathrm{On}\wedge fFnx\wedge y\in x\right)\to if\left(\mathrm{dom}\left({f\upharpoonright }_y\right)=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}\left({f\upharpoonright }_y\right),\bigcup f\left[y\right],F\left(\left({f\upharpoonright }_y\right)\left(\bigcup \mathrm{dom}\left({f\upharpoonright }_y\right)\right)\right)\right)\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)$$
119	41 118	eqtrid	$$⊢\left(x\in \mathrm{On}\wedge fFnx\wedge y\in x\right)\to \left(g\in \mathrm{V}⟼if\left(g=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)\left({f\upharpoonright }_y\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)$$
120	119	eqeq2d	$$⊢\left(x\in \mathrm{On}\wedge fFnx\wedge y\in x\right)\to \left(f\left(y\right)=\left(g\in \mathrm{V}⟼if\left(g=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)\left({f\upharpoonright }_y\right)\leftrightarrow f\left(y\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)$$
121	120	3expa	$$⊢\left(\left(x\in \mathrm{On}\wedge fFnx\right)\wedge y\in x\right)\to \left(f\left(y\right)=\left(g\in \mathrm{V}⟼if\left(g=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)\left({f\upharpoonright }_y\right)\leftrightarrow f\left(y\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)$$
122	121	ralbidva	$$⊢\left(x\in \mathrm{On}\wedge fFnx\right)\to \left(\forall y\in xf\left(y\right)=\left(g\in \mathrm{V}⟼if\left(g=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)\left({f\upharpoonright }_y\right)\leftrightarrow \forall y\in xf\left(y\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)$$
123	122	pm5.32da	$$⊢x\in \mathrm{On}\to \left(\left(fFnx\wedge \forall y\in xf\left(y\right)=\left(g\in \mathrm{V}⟼if\left(g=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)\left({f\upharpoonright }_y\right)\right)\leftrightarrow \left(fFnx\wedge \forall y\in xf\left(y\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)\right)$$
124	123	rexbiia	$$⊢\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=\left(g\in \mathrm{V}⟼if\left(g=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)\left({f\upharpoonright }_y\right)\right)\leftrightarrow \exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)$$
125	124	abbii	$$⊢\left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=\left(g\in \mathrm{V}⟼if\left(g=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)\left({f\upharpoonright }_y\right)\right)\right\}=\left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)\right\}$$
126	125	unieqi	$$⊢\bigcup \left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=\left(g\in \mathrm{V}⟼if\left(g=\varnothing ,i,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)\left({f\upharpoonright }_y\right)\right)\right\}=\bigcup \left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)\right\}$$
127	10 11 126	3eqtri	$$⊢\mathrm{rec}\left(F,i\right)=\bigcup \left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=if\left(y=\varnothing ,i,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)\right\}$$
128	9 127	vtoclg	$$⊢I\in V\to \mathrm{rec}\left(F,I\right)=\bigcup \left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=if\left(y=\varnothing ,I,if\left(\mathrm{Lim}y,\bigcup f\left[y\right],F\left(f\left(\bigcup y\right)\right)\right)\right)\right)\right\}$$