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

Proof

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