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	|- F/_ a F
	setrec2.2	|- B = setrecs ( F )
	setrec2.3	|- ( ph -> A. a ( a C_ C -> ( F ` a ) C_ C ) )
Assertion	setrec2	|- ( ph -> B C_ C )

Proof

Step	Hyp	Ref	Expression
1		setrec2.1	|- F/_ a F
2		setrec2.2	|- B = setrecs ( F )
3		setrec2.3	|- ( ph -> A. a ( a C_ C -> ( F ` a ) C_ C ) )
4		nfcv	|- F/_ a x
5		nfcv	|- F/_ a u
6	4 1 5	nfbr	|- F/ a x F u
7	6	nfeuw	|- F/ a E! u x F u
8	7	nfab	|- F/_ a { x | E! u x F u }
9	1 8	nfres	|- F/_ a ( F |` { x | E! u x F u } )
10		setrec2lem1	|- ( ( F |` { x | E! u x F u } ) ` w ) = ( F ` w )
11	10	sseq1i	|- ( ( ( F |` { x | E! u x F u } ) ` w ) C_ z <-> ( F ` w ) C_ z )
12	11	imbi2i	|- ( ( w C_ z -> ( ( F |` { x | E! u x F u } ) ` w ) C_ z ) <-> ( w C_ z -> ( F ` w ) C_ z ) )
13	12	imbi2i	|- ( ( w C_ y -> ( w C_ z -> ( ( F |` { x | E! u x F u } ) ` w ) C_ z ) ) <-> ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) )
14	13	albii	|- ( A. w ( w C_ y -> ( w C_ z -> ( ( F |` { x | E! u x F u } ) ` w ) C_ z ) ) <-> A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) )
15	14	imbi1i	|- ( ( A. w ( w C_ y -> ( w C_ z -> ( ( F |` { x | E! u x F u } ) ` w ) C_ z ) ) -> y C_ z ) <-> ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) )
16	15	albii	|- ( A. z ( A. w ( w C_ y -> ( w C_ z -> ( ( F |` { x | E! u x F u } ) ` w ) C_ z ) ) -> y C_ z ) <-> A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) )
17	16	abbii	|- { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( ( F |` { x | E! u x F u } ) ` w ) C_ z ) ) -> y C_ z ) } = { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
18	17	unieqi	|- U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( ( F |` { x | E! u x F u } ) ` w ) C_ z ) ) -> y C_ z ) } = U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
19		df-setrecs	|- setrecs ( ( F |` { x | E! u x F u } ) ) = U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( ( F |` { x | E! u x F u } ) ` w ) C_ z ) ) -> y C_ z ) }
20		df-setrecs	|- setrecs ( F ) = U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
21	18 19 20	3eqtr4ri	|- setrecs ( F ) = setrecs ( ( F |` { x | E! u x F u } ) )
22	2 21	eqtri	|- B = setrecs ( ( F |` { x | E! u x F u } ) )
23		setrec2lem2	|- Fun ( F |` { x | E! u x F u } )
24		setrec2lem1	|- ( ( F |` { x | E! u x F u } ) ` a ) = ( F ` a )
25	24	sseq1i	|- ( ( ( F |` { x | E! u x F u } ) ` a ) C_ C <-> ( F ` a ) C_ C )
26	25	imbi2i	|- ( ( a C_ C -> ( ( F |` { x | E! u x F u } ) ` a ) C_ C ) <-> ( a C_ C -> ( F ` a ) C_ C ) )
27	26	albii	|- ( A. a ( a C_ C -> ( ( F |` { x | E! u x F u } ) ` a ) C_ C ) <-> A. a ( a C_ C -> ( F ` a ) C_ C ) )
28	3 27	sylibr	|- ( ph -> A. a ( a C_ C -> ( ( F |` { x | E! u x F u } ) ` a ) C_ C ) )
29	9 22 23 28	setrec2fun	|- ( ph -> B C_ C )