Theorem setrec2fun 42439

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 42438 and setrec2v 42443 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 7053) to the other class.

(Contributed by Emmett Weisz, 15-Feb-2021.) (New usage is discouraged.)

Hypotheses

Ref	Expression
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

Ref	Expression
setrec2fun	|- ( ph -> B C_ C )

Distinct variable group:   C, a

Allowed substitution hints:   ph( a)   B( a)   F( a)

Proof of Theorem setrec2fun

Dummy variables x w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		setrec2fun.2	. . 3 |- B = setrecs ( F )
2		df-setrecs 42431	. . 3 |- setrecs ( F ) = U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
3	1, 2	eqtri 2644	. 2 |- B = U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
4		eqid 2622	. . . . . 6 |- { 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 ) }
5		vex 3203	. . . . . . 7 |- x e. _V
6	5	a1i 11	. . . . . 6 |- ( ph -> x e. _V )
7	4, 6	setrec1lem1 42434	. . . . 5 |- ( 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 ) ) )
8		id 22	. . . . . . . . . . . . . . 15 |- ( w C_ ( C i^i U. ( F " ~P x ) ) -> w C_ ( C i^i U. ( F " ~P x ) ) )
9		inss1 3833	. . . . . . . . . . . . . . 15 |- ( C i^i U. ( F " ~P x ) ) C_ C
10	8, 9	syl6ss 3615	. . . . . . . . . . . . . 14 |- ( w C_ ( C i^i U. ( F " ~P x ) ) -> w C_ C )
11		setrec2fun.4	. . . . . . . . . . . . . . 15 |- ( ph -> A. a ( a C_ C -> ( F ` a ) C_ C ) )
12		nfv 1843	. . . . . . . . . . . . . . . . 17 |- F/ a w C_ C
13		setrec2fun.1	. . . . . . . . . . . . . . . . . . 19 |- F/_ a F
14		nfcv 2764	. . . . . . . . . . . . . . . . . . 19 |- F/_ a w
15	13, 14	nffv 6198	. . . . . . . . . . . . . . . . . 18 |- F/_ a ( F ` w )
16		nfcv 2764	. . . . . . . . . . . . . . . . . 18 |- F/_ a C
17	15, 16	nfss 3596	. . . . . . . . . . . . . . . . 17 |- F/ a ( F ` w ) C_ C
18	12, 17	nfim 1825	. . . . . . . . . . . . . . . 16 |- F/ a ( w C_ C -> ( F ` w ) C_ C )
19		sseq1 3626	. . . . . . . . . . . . . . . . . 18 |- ( a = w -> ( a C_ C <-> w C_ C ) )
20		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 |- ( a = w -> ( F ` a ) = ( F ` w ) )
21	20	sseq1d 3632	. . . . . . . . . . . . . . . . . 18 |- ( a = w -> ( ( F ` a ) C_ C <-> ( F ` w ) C_ C ) )
22	19, 21	imbi12d 334	. . . . . . . . . . . . . . . . 17 |- ( a = w -> ( ( a C_ C -> ( F ` a ) C_ C ) <-> ( w C_ C -> ( F ` w ) C_ C ) ) )
23	22	biimpd 219	. . . . . . . . . . . . . . . 16 |- ( a = w -> ( ( a C_ C -> ( F ` a ) C_ C ) -> ( w C_ C -> ( F ` w ) C_ C ) ) )
24	18, 23	spim 2254	. . . . . . . . . . . . . . 15 |- ( A. a ( a C_ C -> ( F ` a ) C_ C ) -> ( w C_ C -> ( F ` w ) C_ C ) )
25	11, 24	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> ( w C_ C -> ( F ` w ) C_ C ) )
26	10, 25	syl5 34	. . . . . . . . . . . . 13 |- ( ph -> ( w C_ ( C i^i U. ( F " ~P x ) ) -> ( F ` w ) C_ C ) )
27	26	imp 445	. . . . . . . . . . . 12 |- ( ( ph /\ w C_ ( C i^i U. ( F " ~P x ) ) ) -> ( F ` w ) C_ C )
28	27	3adant2 1080	. . . . . . . . . . 11 |- ( ( ph /\ w C_ x /\ w C_ ( C i^i U. ( F " ~P x ) ) ) -> ( F ` w ) C_ C )
29		selpw 4165	. . . . . . . . . . . . . . 15 |- ( w e. ~P x <-> w C_ x )
30		eliman0 6223	. . . . . . . . . . . . . . . 16 |- ( ( w e. ~P x /\ -. ( F ` w ) = (/) ) -> ( F ` w ) e. ( F " ~P x ) )
31	30	ex 450	. . . . . . . . . . . . . . 15 |- ( w e. ~P x -> ( -. ( F ` w ) = (/) -> ( F ` w ) e. ( F " ~P x ) ) )
32	29, 31	sylbir 225	. . . . . . . . . . . . . 14 |- ( w C_ x -> ( -. ( F ` w ) = (/) -> ( F ` w ) e. ( F " ~P x ) ) )
33		elssuni 4467	. . . . . . . . . . . . . 14 |- ( ( F ` w ) e. ( F " ~P x ) -> ( F ` w ) C_ U. ( F " ~P x ) )
34	32, 33	syl6 35	. . . . . . . . . . . . 13 |- ( w C_ x -> ( -. ( F ` w ) = (/) -> ( F ` w ) C_ U. ( F " ~P x ) ) )
35		id 22	. . . . . . . . . . . . . 14 |- ( ( F ` w ) = (/) -> ( F ` w ) = (/) )
36		0ss 3972	. . . . . . . . . . . . . 14 |- (/) C_ U. ( F " ~P x )
37	35, 36	syl6eqss 3655	. . . . . . . . . . . . 13 |- ( ( F ` w ) = (/) -> ( F ` w ) C_ U. ( F " ~P x ) )
38	34, 37	pm2.61d2 172	. . . . . . . . . . . 12 |- ( w C_ x -> ( F ` w ) C_ U. ( F " ~P x ) )
39	38	3ad2ant2 1083	. . . . . . . . . . 11 |- ( ( ph /\ w C_ x /\ w C_ ( C i^i U. ( F " ~P x ) ) ) -> ( F ` w ) C_ U. ( F " ~P x ) )
40	28, 39	ssind 3837	. . . . . . . . . 10 |- ( ( ph /\ w C_ x /\ w C_ ( C i^i U. ( F " ~P x ) ) ) -> ( F ` w ) C_ ( C i^i U. ( F " ~P x ) ) )
41	40	3exp 1264	. . . . . . . . 9 |- ( 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	alrimiv 1855	. . . . . . . 8 |- ( 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 ) ) ) ) )
43		setrec2fun.3	. . . . . . . . . . . 12 |- Fun F
44	5	pwex 4848	. . . . . . . . . . . . 13 |- ~P x e. _V
45	44	funimaex 5976	. . . . . . . . . . . 12 |- ( Fun F -> ( F " ~P x ) e. _V )
46	43, 45	ax-mp 5	. . . . . . . . . . 11 |- ( F " ~P x ) e. _V
47	46	uniex 6953	. . . . . . . . . 10 |- U. ( F " ~P x ) e. _V
48	47	inex2 4800	. . . . . . . . 9 |- ( C i^i U. ( F " ~P x ) ) e. _V
49		sseq2 3627	. . . . . . . . . . . . 13 |- ( z = ( C i^i U. ( F " ~P x ) ) -> ( w C_ z <-> w C_ ( C i^i U. ( F " ~P x ) ) ) )
50		sseq2 3627	. . . . . . . . . . . . 13 |- ( 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 334	. . . . . . . . . . . 12 |- ( 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 330	. . . . . . . . . . 11 |- ( 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 1849	. . . . . . . . . 10 |- ( 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 3627	. . . . . . . . . 10 |- ( z = ( C i^i U. ( F " ~P x ) ) -> ( x C_ z <-> x C_ ( C i^i U. ( F " ~P x ) ) ) )
55	53, 54	imbi12d 334	. . . . . . . . 9 |- ( 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 3299	. . . . . . . 8 |- ( 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	42, 56	mpan9 486	. . . . . . 7 |- ( ( 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, 9	syl6ss 3615	. . . . . 6 |- ( ( ph /\ A. z ( A. w ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z ) ) -> x C_ C )
59	58	ex 450	. . . . 5 |- ( ph -> ( A. z ( A. w ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z ) -> x C_ C ) )
60	7, 59	sylbid 230	. . . 4 |- ( 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 2965	. . 3 |- ( 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 4469	. . 3 |- ( 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 224	. 2 |- ( ph -> U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } C_ C )
64	3, 63	syl5eqss 3649	1 |- ( ph -> B C_ C )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   /\ w3a 1037   A.wal 1481   = wceq 1483   e. wcel 1990   {cab 2608   F/_wnfc 2751   A.wral 2912   _Vcvv 3200   i^i cin 3573   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   U.cuni 4436   "cima 5117   Fun wfun 5882   ` cfv 5888  setrecscsetrecs 42430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fv 5896  df-setrecs 42431

This theorem is referenced by:  setrec2  42442