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	$⊢ \underline{Ⅎ} a F$
	setrec2fun.2	$⊢ B = setrecs (F)$
	setrec2fun.3	$⊢ Fun F$
	setrec2fun.4	$⊢ φ \to \forall a (a \subseteq C \to F (a) \subseteq C)$
Assertion	setrec2fun	$⊢ φ \to B \subseteq C$

Proof

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

Metamath Proof Explorer

Theorem setrec2fun

Proof