Theorem setrec2fun

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 say that setrecs ( F ) is 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, 15-Feb-2021) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		setrec2fun.1	$$⊢\underset{\_}{Ⅎ}aF$$
2		setrec2fun.2	$$⊢B=\mathrm{setrecs}\left(F\right)$$
3		setrec2fun.3	$$⊢\mathrm{Fun}F$$
4		setrec2fun.4	$$⊢\phi \to \forall a\left(a\subseteq C\to F\left(a\right)\subseteq C\right)$$
5		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\}$$
6	2 5	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\}$$
7		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\}$$
8		vex	$$⊢x\in \mathrm{V}$$
9	8	a1i	$$⊢\phi \to x\in \mathrm{V}$$
10	7 9	setrec1lem1	$$⊢\phi \to \left(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\}\leftrightarrow \forall z\left(\forall w\left(w\subseteq x\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to x\subseteq z\right)\right)$$
11		id	$$⊢w\subseteq C\cap \bigcup F\left[𝒫x\right]\to w\subseteq C\cap \bigcup F\left[𝒫x\right]$$
12		inss1	$$⊢C\cap \bigcup F\left[𝒫x\right]\subseteq C$$
13	11 12	sstrdi	$$⊢w\subseteq C\cap \bigcup F\left[𝒫x\right]\to w\subseteq C$$
14		nfv	$$⊢Ⅎaw\subseteq C$$
15		nfcv	$$⊢\underset{\_}{Ⅎ}aw$$
16	1 15	nffv	$$⊢\underset{\_}{Ⅎ}aF\left(w\right)$$
17		nfcv	$$⊢\underset{\_}{Ⅎ}aC$$
18	16 17	nfss	$$⊢ℲaF\left(w\right)\subseteq C$$
19	14 18	nfim	$$⊢Ⅎa\left(w\subseteq C\to F\left(w\right)\subseteq C\right)$$
20		sseq1	$$⊢a=w\to \left(a\subseteq C\leftrightarrow w\subseteq C\right)$$
21		fveq2	$$⊢a=w\to F\left(a\right)=F\left(w\right)$$
22	21	sseq1d	$$⊢a=w\to \left(F\left(a\right)\subseteq C\leftrightarrow F\left(w\right)\subseteq C\right)$$
23	20 22	imbi12d	$$⊢a=w\to \left(\left(a\subseteq C\to F\left(a\right)\subseteq C\right)\leftrightarrow \left(w\subseteq C\to F\left(w\right)\subseteq C\right)\right)$$
24	23	biimpd	$$⊢a=w\to \left(\left(a\subseteq C\to F\left(a\right)\subseteq C\right)\to \left(w\subseteq C\to F\left(w\right)\subseteq C\right)\right)$$
25	19 24	spimfv	$$⊢\forall a\left(a\subseteq C\to F\left(a\right)\subseteq C\right)\to \left(w\subseteq C\to F\left(w\right)\subseteq C\right)$$
26	4 25	syl	$$⊢\phi \to \left(w\subseteq C\to F\left(w\right)\subseteq C\right)$$
27	13 26	syl5	$$⊢\phi \to \left(w\subseteq C\cap \bigcup F\left[𝒫x\right]\to F\left(w\right)\subseteq C\right)$$
28	27	imp	$$⊢\left(\phi \wedge w\subseteq C\cap \bigcup F\left[𝒫x\right]\right)\to F\left(w\right)\subseteq C$$
29	28	3adant2	$$⊢\left(\phi \wedge w\subseteq x\wedge w\subseteq C\cap \bigcup F\left[𝒫x\right]\right)\to F\left(w\right)\subseteq C$$
30		velpw	$$⊢w\in 𝒫x\leftrightarrow w\subseteq x$$
31		eliman0	$$⊢\left(w\in 𝒫x\wedge \neg F\left(w\right)=\varnothing \right)\to F\left(w\right)\in F\left[𝒫x\right]$$
32	31	ex	$$⊢w\in 𝒫x\to \left(\neg F\left(w\right)=\varnothing \to F\left(w\right)\in F\left[𝒫x\right]\right)$$
33	30 32	sylbir	$$⊢w\subseteq x\to \left(\neg F\left(w\right)=\varnothing \to F\left(w\right)\in F\left[𝒫x\right]\right)$$
34		elssuni	$$⊢F\left(w\right)\in F\left[𝒫x\right]\to F\left(w\right)\subseteq \bigcup F\left[𝒫x\right]$$
35	33 34	syl6	$$⊢w\subseteq x\to \left(\neg F\left(w\right)=\varnothing \to F\left(w\right)\subseteq \bigcup F\left[𝒫x\right]\right)$$
36		id	$$⊢F\left(w\right)=\varnothing \to F\left(w\right)=\varnothing$$
37		0ss	$$⊢\varnothing \subseteq \bigcup F\left[𝒫x\right]$$
38	36 37	eqsstrdi	$$⊢F\left(w\right)=\varnothing \to F\left(w\right)\subseteq \bigcup F\left[𝒫x\right]$$
39	35 38	pm2.61d2	$$⊢w\subseteq x\to F\left(w\right)\subseteq \bigcup F\left[𝒫x\right]$$
40	39	3ad2ant2	$$⊢\left(\phi \wedge w\subseteq x\wedge w\subseteq C\cap \bigcup F\left[𝒫x\right]\right)\to F\left(w\right)\subseteq \bigcup F\left[𝒫x\right]$$
41	29 40	ssind	$$⊢\left(\phi \wedge w\subseteq x\wedge w\subseteq C\cap \bigcup F\left[𝒫x\right]\right)\to F\left(w\right)\subseteq C\cap \bigcup F\left[𝒫x\right]$$
42	41	3exp	$$⊢\phi \to \left(w\subseteq x\to \left(w\subseteq C\cap \bigcup F\left[𝒫x\right]\to F\left(w\right)\subseteq C\cap \bigcup F\left[𝒫x\right]\right)\right)$$
43	42	alrimiv	$$⊢\phi \to \forall w\left(w\subseteq x\to \left(w\subseteq C\cap \bigcup F\left[𝒫x\right]\to F\left(w\right)\subseteq C\cap \bigcup F\left[𝒫x\right]\right)\right)$$
44	8	pwex	$$⊢𝒫x\in \mathrm{V}$$
45	44	funimaex	$$⊢\mathrm{Fun}F\to F\left[𝒫x\right]\in \mathrm{V}$$
46	3 45	ax-mp	$$⊢F\left[𝒫x\right]\in \mathrm{V}$$
47	46	uniex	$$⊢\bigcup F\left[𝒫x\right]\in \mathrm{V}$$
48	47	inex2	$$⊢C\cap \bigcup F\left[𝒫x\right]\in \mathrm{V}$$
49		sseq2	$$⊢z=C\cap \bigcup F\left[𝒫x\right]\to \left(w\subseteq z\leftrightarrow w\subseteq C\cap \bigcup F\left[𝒫x\right]\right)$$
50		sseq2	$$⊢z=C\cap \bigcup F\left[𝒫x\right]\to \left(F\left(w\right)\subseteq z\leftrightarrow F\left(w\right)\subseteq C\cap \bigcup F\left[𝒫x\right]\right)$$
51	49 50	imbi12d	$$⊢z=C\cap \bigcup F\left[𝒫x\right]\to \left(\left(w\subseteq z\to F\left(w\right)\subseteq z\right)\leftrightarrow \left(w\subseteq C\cap \bigcup F\left[𝒫x\right]\to F\left(w\right)\subseteq C\cap \bigcup F\left[𝒫x\right]\right)\right)$$
52	51	imbi2d	$$⊢z=C\cap \bigcup F\left[𝒫x\right]\to \left(\left(w\subseteq x\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\leftrightarrow \left(w\subseteq x\to \left(w\subseteq C\cap \bigcup F\left[𝒫x\right]\to F\left(w\right)\subseteq C\cap \bigcup F\left[𝒫x\right]\right)\right)\right)$$
53	52	albidv	$$⊢z=C\cap \bigcup F\left[𝒫x\right]\to \left(\forall w\left(w\subseteq x\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\leftrightarrow \forall w\left(w\subseteq x\to \left(w\subseteq C\cap \bigcup F\left[𝒫x\right]\to F\left(w\right)\subseteq C\cap \bigcup F\left[𝒫x\right]\right)\right)\right)$$
54		sseq2	$$⊢z=C\cap \bigcup F\left[𝒫x\right]\to \left(x\subseteq z\leftrightarrow x\subseteq C\cap \bigcup F\left[𝒫x\right]\right)$$
55	53 54	imbi12d	$$⊢z=C\cap \bigcup F\left[𝒫x\right]\to \left(\left(\forall w\left(w\subseteq x\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to x\subseteq z\right)\leftrightarrow \left(\forall w\left(w\subseteq x\to \left(w\subseteq C\cap \bigcup F\left[𝒫x\right]\to F\left(w\right)\subseteq C\cap \bigcup F\left[𝒫x\right]\right)\right)\to x\subseteq C\cap \bigcup F\left[𝒫x\right]\right)\right)$$
56	48 55	spcv	$$⊢\forall z\left(\forall w\left(w\subseteq x\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to x\subseteq z\right)\to \left(\forall w\left(w\subseteq x\to \left(w\subseteq C\cap \bigcup F\left[𝒫x\right]\to F\left(w\right)\subseteq C\cap \bigcup F\left[𝒫x\right]\right)\right)\to x\subseteq C\cap \bigcup F\left[𝒫x\right]\right)$$
57	43 56	mpan9	$$⊢\left(\phi \wedge \forall z\left(\forall w\left(w\subseteq x\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to x\subseteq z\right)\right)\to x\subseteq C\cap \bigcup F\left[𝒫x\right]$$
58	57 12	sstrdi	$$⊢\left(\phi \wedge \forall z\left(\forall w\left(w\subseteq x\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to x\subseteq z\right)\right)\to x\subseteq C$$
59	58	ex	$$⊢\phi \to \left(\forall z\left(\forall w\left(w\subseteq x\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to x\subseteq z\right)\to x\subseteq C\right)$$
60	10 59	sylbid	$$⊢\phi \to \left(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\}\to x\subseteq C\right)$$
61	60	ralrimiv	$$⊢\phi \to \forall 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\}x\subseteq C$$
62		unissb	$$⊢\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\}\subseteq C\leftrightarrow \forall 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\}x\subseteq C$$
63	61 62	sylibr	$$⊢\phi \to \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\}\subseteq C$$
64	6 63	eqsstrid	$$⊢\phi \to B\subseteq C$$