Theorem setrec1

Description: This is the first of two fundamental theorems about set recursion from which all other facts will be derived. It states that the class setrecs ( F ) is closed under F . This effectively sets the actual value of setrecs ( F ) as a lower bound for setrecs ( F ) , as it implies that any set generated by successive applications of F is a member of B . This theorem "gets off the ground" because we can start by letting A = (/) , and the hypotheses of the theorem will hold trivially.

Variable B represents an abbreviation of setrecs ( F ) or another name of setrecs ( F ) (for an example of the latter, see theorem setrecon).

Proof summary: Assume that A C_ B , meaning that all elements of A are in some set recursively generated by F . Then by setrec1lem3 , A is a subset of some set recursively generated by F . (It turns out that A itself is recursively generated by F , but we don't need this fact. See the comment to setrec1lem3 .) Therefore, by setrec1lem4 , ( FA ) is a subset of some set recursively generated by F . Thus, by ssuni , it is a subset of the union of all sets recursively generated by F .

See df-setrecs for a detailed description of how the setrecs definition works.

(Contributed by Emmett Weisz, 9-Oct-2020)

	Ref	Expression
Hypotheses	setrec1.b	$$⊢B=\mathrm{setrecs}\left(F\right)$$
	setrec1.v	$$⊢\phi \to A\in \mathrm{V}$$
	setrec1.a	$$⊢\phi \to A\subseteq B$$
Assertion	setrec1	$$⊢\phi \to F\left(A\right)\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		setrec1.b	$$⊢B=\mathrm{setrecs}\left(F\right)$$
2		setrec1.v	$$⊢\phi \to A\in \mathrm{V}$$
3		setrec1.a	$$⊢\phi \to A\subseteq B$$
4		eqid	$$⊢\left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}=\left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
5	3	sseld	$$⊢\phi \to \left(a\in A\to a\in B\right)$$
6	5	imp	$$⊢\left(\phi \wedge a\in A\right)\to a\in B$$
7		df-setrecs	$$⊢\mathrm{setrecs}\left(F\right)=\bigcup \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
8	1 7	eqtri	$$⊢B=\bigcup \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
9	6 8	eleqtrdi	$$⊢\left(\phi \wedge a\in A\right)\to a\in \bigcup \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
10		eluni	$$⊢a\in \bigcup \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}\leftrightarrow \exists x\left(a\in x\wedge x\in \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}\right)$$
11	9 10	sylib	$$⊢\left(\phi \wedge a\in A\right)\to \exists x\left(a\in x\wedge x\in \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}\right)$$
12	11	ralrimiva	$$⊢\phi \to \forall a\in A\exists x\left(a\in x\wedge x\in \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}\right)$$
13	4 2 12	setrec1lem3	$$⊢\phi \to \exists x\left(A\subseteq x\wedge x\in \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}\right)$$
14		nfv	$$⊢Ⅎz\phi$$
15		nfv	$$⊢ℲzA\subseteq x$$
16		nfaba1	$$⊢\underset{\_}{Ⅎ}z\left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
17	16	nfel2	$$⊢Ⅎzx\in \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
18	15 17	nfan	$$⊢Ⅎz\left(A\subseteq x\wedge x\in \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}\right)$$
19	14 18	nfan	$$⊢Ⅎz\left(\phi \wedge \left(A\subseteq x\wedge x\in \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}\right)\right)$$
20	2	adantr	$$⊢\left(\phi \wedge \left(A\subseteq x\wedge x\in \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}\right)\right)\to A\in \mathrm{V}$$
21		simprl	$$⊢\left(\phi \wedge \left(A\subseteq x\wedge x\in \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}\right)\right)\to A\subseteq x$$
22		simprr	$$⊢\left(\phi \wedge \left(A\subseteq x\wedge x\in \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}\right)\right)\to x\in \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
23	19 4 20 21 22	setrec1lem4	$$⊢\left(\phi \wedge \left(A\subseteq x\wedge x\in \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}\right)\right)\to x\cup F\left(A\right)\in \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
24		ssun2	$$⊢F\left(A\right)\subseteq x\cup F\left(A\right)$$
25	23 24	jctil	$$⊢\left(\phi \wedge \left(A\subseteq x\wedge x\in \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}\right)\right)\to \left(F\left(A\right)\subseteq x\cup F\left(A\right)\wedge x\cup F\left(A\right)\in \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}\right)$$
26		ssuni	$$⊢\left(F\left(A\right)\subseteq x\cup F\left(A\right)\wedge x\cup F\left(A\right)\in \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}\right)\to F\left(A\right)\subseteq \bigcup \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
27	25 26	syl	$$⊢\left(\phi \wedge \left(A\subseteq x\wedge x\in \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}\right)\right)\to F\left(A\right)\subseteq \bigcup \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
28	13 27	exlimddv	$$⊢\phi \to F\left(A\right)\subseteq \bigcup \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
29	28 8	sseqtrrdi	$$⊢\phi \to F\left(A\right)\subseteq B$$