Theorem setrec2

Description: This is the second of two fundamental theorems about set recursion from which all other facts will be derived. It states that the class setrecs ( F ) is a subclass of all classes C that are closed under F . Taken together, theorems setrec1 and setrec2v uniquely determine setrecs ( F ) to be the minimal class closed under F .

We express this by saying that if F respects the C_ relation and C is closed under F , then B C_ C . By substituting strategically constructed classes for C , we can easily prove many useful properties. Although this theorem cannot show equality between B and C , if we intend to prove equality between B and some particular class (such as On ), we first apply this theorem, then the relevant induction theorem (such as tfi ) to the other class.

(Contributed by Emmett Weisz, 2-Sep-2021)

	Ref	Expression
Hypotheses	setrec2.1	$$⊢\underset{\_}{Ⅎ}aF$$
	setrec2.2	$$⊢B=\mathrm{setrecs}\left(F\right)$$
	setrec2.3	$$⊢\phi \to \forall a\left(a\subseteq C\to F\left(a\right)\subseteq C\right)$$
Assertion	setrec2	$$⊢\phi \to B\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		setrec2.1	$$⊢\underset{\_}{Ⅎ}aF$$
2		setrec2.2	$$⊢B=\mathrm{setrecs}\left(F\right)$$
3		setrec2.3	$$⊢\phi \to \forall a\left(a\subseteq C\to F\left(a\right)\subseteq C\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}ax$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}au$$
6	4 1 5	nfbr	$$⊢ℲaxFu$$
7	6	nfeuw	$$⊢Ⅎa\exists !uxFu$$
8	7	nfab	$$⊢\underset{\_}{Ⅎ}a\left\{x|\exists !uxFu\right\}$$
9	1 8	nfres	$$⊢\underset{\_}{Ⅎ}a\left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)$$
10		setrec2lem1	$$⊢\left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\left(w\right)=F\left(w\right)$$
11	10	sseq1i	$$⊢\left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\left(w\right)\subseteq z\leftrightarrow F\left(w\right)\subseteq z$$
12	11	imbi2i	$$⊢\left(w\subseteq z\to \left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\left(w\right)\subseteq z\right)\leftrightarrow \left(w\subseteq z\to F\left(w\right)\subseteq z\right)$$
13	12	imbi2i	$$⊢\left(w\subseteq y\to \left(w\subseteq z\to \left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\left(w\right)\subseteq z\right)\right)\leftrightarrow \left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)$$
14	13	albii	$$⊢\forall w\left(w\subseteq y\to \left(w\subseteq z\to \left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\left(w\right)\subseteq z\right)\right)\leftrightarrow \forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)$$
15	14	imbi1i	$$⊢\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to \left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\leftrightarrow \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)$$
16	15	albii	$$⊢\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to \left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\leftrightarrow \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)$$
17	16	abbii	$$⊢\left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to \left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\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\}$$
18	17	unieqi	$$⊢\bigcup \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to \left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\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\}$$
19		df-setrecs	$$⊢\mathrm{setrecs}\left(\left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\right)=\bigcup \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to \left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
20		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\}$$
21	18 19 20	3eqtr4ri	$$⊢\mathrm{setrecs}\left(F\right)=\mathrm{setrecs}\left(\left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\right)$$
22	2 21	eqtri	$$⊢B=\mathrm{setrecs}\left(\left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\right)$$
23		setrec2lem2	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)$$
24		setrec2lem1	$$⊢\left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\left(a\right)=F\left(a\right)$$
25	24	sseq1i	$$⊢\left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\left(a\right)\subseteq C\leftrightarrow F\left(a\right)\subseteq C$$
26	25	imbi2i	$$⊢\left(a\subseteq C\to \left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\left(a\right)\subseteq C\right)\leftrightarrow \left(a\subseteq C\to F\left(a\right)\subseteq C\right)$$
27	26	albii	$$⊢\forall a\left(a\subseteq C\to \left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\left(a\right)\subseteq C\right)\leftrightarrow \forall a\left(a\subseteq C\to F\left(a\right)\subseteq C\right)$$
28	3 27	sylibr	$$⊢\phi \to \forall a\left(a\subseteq C\to \left({F\upharpoonright }_{\left\{x|\exists !uxFu\right\}}\right)\left(a\right)\subseteq C\right)$$
29	9 22 23 28	setrec2fun	$$⊢\phi \to B\subseteq C$$