Definition df-setrecs

Description: Define a class setrecs ( F ) by transfinite recursion, where ( Fx ) is the set of new elements to add to the class given the set x of elements in the class so far. We do not need a base case, because we can start with the empty set, which is vacuously a subset of setrecs ( F ) . The goal of this definition is to construct a class fulfilling Theorems setrec1 and setrec2v , which give a more intuitive idea of the meaning of setrecs . Unlike wrecs , setrecs is well-defined for any F and meaningful for any function F .

The definition works by building subsets of the desired class and taking the union of those subsets. To find such a collection of subsets, consider an arbitrary set z , and consider the result when applying F to any subset w C_ z . Remember that F can be any function, and in general we are interested in functions that give outputs that are larger than their inputs, so we have no reason to expect the outputs to be within z . However, if we restrict the domain of F to a given set y , the resulting range will be a set. Therefore, with this restricted F , it makes sense to consider sets z that are closed under F applied to its subsets. Now we can test whether a given set y is recursively generated by F . If every set z that is closed under F contains y , that means that every member of y must eventually be generated by F . On the other hand, if some such z does not contain a certain element of y , then that element can be avoided even if we apply F in every possible way to previously generated elements.

For an example, see Theorem onsetrec for how the class On is defined recursively using the successor function.

(Contributed by Emmett Weisz, 18-Aug-2020) (New usage is discouraged.)

	Ref	Expression
Assertion	df-setrecs	|- setrecs ( F ) = U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	|- F
1	0	csetrecs	|- setrecs ( F )
2		vy	|- y
3		vz	|- z
4		vw	|- w
5	4	cv	|- w
6	2	cv	|- y
7	5 6	wss	|- w C_ y
8	3	cv	|- z
9	5 8	wss	|- w C_ z
10	5 0	cfv	|- ( F ` w )
11	10 8	wss	|- ( F ` w ) C_ z
12	9 11	wi	|- ( w C_ z -> ( F ` w ) C_ z )
13	7 12	wi	|- ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) )
14	13 4	wal	|- A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) )
15	6 8	wss	|- y C_ z
16	14 15	wi	|- ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z )
17	16 3	wal	|- A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z )
18	17 2	cab	|- { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
19	18	cuni	|- U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
20	1 19	wceq	|- setrecs ( F ) = U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }