Theorem setrec1lem2

Description: Lemma for setrec1 . If a family of sets are all recursively generated by F , so is their union. In this theorem, X is a family of sets which are all elements of Y , and V is any class. Use dfss3 , equivalence and equality theorems, and unissb at the end. Sandwich with applications of setrec1lem1. (Contributed by Emmett Weisz, 24-Jan-2021) (New usage is discouraged.)

	Ref	Expression
Hypotheses	setrec1lem2.1	|- Y = { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
	setrec1lem2.2	|- ( ph -> X e. V )
	setrec1lem2.3	|- ( ph -> X C_ Y )
Assertion	setrec1lem2	|- ( ph -> U. X e. Y )

Proof

Step	Hyp	Ref	Expression
1		setrec1lem2.1	|- Y = { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
2		setrec1lem2.2	|- ( ph -> X e. V )
3		setrec1lem2.3	|- ( ph -> X C_ Y )
4		dfss3	|- ( X C_ Y <-> A. x e. X x e. Y )
5	3 4	sylib	|- ( ph -> A. x e. X x e. Y )
6		vex	|- x e. _V
7	6	a1i	|- ( ph -> x e. _V )
8	1 7	setrec1lem1	|- ( ph -> ( x e. Y <-> A. z ( A. w ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z ) ) )
9	8	ralbidv	|- ( ph -> ( A. x e. X x e. Y <-> A. x e. X A. z ( A. w ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z ) ) )
10	5 9	mpbid	|- ( ph -> A. x e. X A. z ( A. w ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z ) )
11		ralcom4	|- ( A. x e. X A. z ( A. w ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z ) <-> A. z A. x e. X ( A. w ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z ) )
12	10 11	sylib	|- ( ph -> A. z A. x e. X ( A. w ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z ) )
13		nfra1	|- F/ x A. x e. X ( A. w ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z )
14		nfv	|- F/ x A. w ( w C_ U. X -> ( w C_ z -> ( F ` w ) C_ z ) )
15		rsp	|- ( A. x e. X ( A. w ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z ) -> ( x e. X -> ( A. w ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z ) ) )
16		elssuni	|- ( x e. X -> x C_ U. X )
17		sstr2	|- ( w C_ x -> ( x C_ U. X -> w C_ U. X ) )
18	16 17	syl5com	|- ( x e. X -> ( w C_ x -> w C_ U. X ) )
19	18	imim1d	|- ( x e. X -> ( ( w C_ U. X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) ) )
20	19	alimdv	|- ( x e. X -> ( A. w ( w C_ U. X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> A. w ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) ) )
21	20	imim1d	|- ( x e. X -> ( ( A. w ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z ) -> ( A. w ( w C_ U. X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z ) ) )
22	15 21	sylcom	|- ( A. x e. X ( A. w ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z ) -> ( x e. X -> ( A. w ( w C_ U. X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z ) ) )
23	22	com23	|- ( A. x e. X ( A. w ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z ) -> ( A. w ( w C_ U. X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> ( x e. X -> x C_ z ) ) )
24	13 14 23	ralrimd	|- ( A. x e. X ( A. w ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z ) -> ( A. w ( w C_ U. X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> A. x e. X x C_ z ) )
25	24	alimi	|- ( A. z A. x e. X ( A. w ( w C_ x -> ( w C_ z -> ( F ` w ) C_ z ) ) -> x C_ z ) -> A. z ( A. w ( w C_ U. X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> A. x e. X x C_ z ) )
26	12 25	syl	|- ( ph -> A. z ( A. w ( w C_ U. X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> A. x e. X x C_ z ) )
27		unissb	|- ( U. X C_ z <-> A. x e. X x C_ z )
28	27	imbi2i	|- ( ( A. w ( w C_ U. X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> U. X C_ z ) <-> ( A. w ( w C_ U. X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> A. x e. X x C_ z ) )
29	28	albii	|- ( A. z ( A. w ( w C_ U. X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> U. X C_ z ) <-> A. z ( A. w ( w C_ U. X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> A. x e. X x C_ z ) )
30	26 29	sylibr	|- ( ph -> A. z ( A. w ( w C_ U. X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> U. X C_ z ) )
31	2	uniexd	|- ( ph -> U. X e. _V )
32	1 31	setrec1lem1	|- ( ph -> ( U. X e. Y <-> A. z ( A. w ( w C_ U. X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> U. X C_ z ) ) )
33	30 32	mpbird	|- ( ph -> U. X e. Y )