Theorem setrec1lem3

Description: Lemma for setrec1 . If each element a of A is covered by a set x recursively generated by F , then there is a single such set covering all of A . The set is constructed explicitly using setrec1lem2 . It turns out that x = A also works, i.e., given the hypotheses it is possible to prove that A e. Y . I don't know if proving this fact directly using setrec1lem1 would be any easier than the current proof using setrec1lem2 , and it would only slightly simplify the proof of setrec1 . Other than the use of bnd2d , this is a purely technical theorem for rearranging notation from that of setrec1lem2 to that of setrec1 . (Contributed by Emmett Weisz, 20-Jan-2021) (New usage is discouraged.)

	Ref	Expression
Hypotheses	setrec1lem3.1	|- Y = { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
	setrec1lem3.2	|- ( ph -> A e. _V )
	setrec1lem3.3	|- ( ph -> A. a e. A E. x ( a e. x /\ x e. Y ) )
Assertion	setrec1lem3	|- ( ph -> E. x ( A C_ x /\ x e. Y ) )

Proof

Step	Hyp	Ref	Expression
1		setrec1lem3.1	|- Y = { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
2		setrec1lem3.2	|- ( ph -> A e. _V )
3		setrec1lem3.3	|- ( ph -> A. a e. A E. x ( a e. x /\ x e. Y ) )
4		exancom	|- ( E. x ( a e. x /\ x e. Y ) <-> E. x ( x e. Y /\ a e. x ) )
5	4	ralbii	|- ( A. a e. A E. x ( a e. x /\ x e. Y ) <-> A. a e. A E. x ( x e. Y /\ a e. x ) )
6	3 5	sylib	|- ( ph -> A. a e. A E. x ( x e. Y /\ a e. x ) )
7		df-rex	|- ( E. x e. Y a e. x <-> E. x ( x e. Y /\ a e. x ) )
8	7	ralbii	|- ( A. a e. A E. x e. Y a e. x <-> A. a e. A E. x ( x e. Y /\ a e. x ) )
9	6 8	sylibr	|- ( ph -> A. a e. A E. x e. Y a e. x )
10	2 9	bnd2d	|- ( ph -> E. v ( v C_ Y /\ A. a e. A E. x e. v a e. x ) )
11		exancom	|- ( E. x ( x e. v /\ a e. x ) <-> E. x ( a e. x /\ x e. v ) )
12		df-rex	|- ( E. x e. v a e. x <-> E. x ( x e. v /\ a e. x ) )
13		eluni	|- ( a e. U. v <-> E. x ( a e. x /\ x e. v ) )
14	11 12 13	3bitr4i	|- ( E. x e. v a e. x <-> a e. U. v )
15	14	ralbii	|- ( A. a e. A E. x e. v a e. x <-> A. a e. A a e. U. v )
16		dfss3	|- ( A C_ U. v <-> A. a e. A a e. U. v )
17	15 16	bitr4i	|- ( A. a e. A E. x e. v a e. x <-> A C_ U. v )
18	17	anbi2i	|- ( ( v C_ Y /\ A. a e. A E. x e. v a e. x ) <-> ( v C_ Y /\ A C_ U. v ) )
19	18	exbii	|- ( E. v ( v C_ Y /\ A. a e. A E. x e. v a e. x ) <-> E. v ( v C_ Y /\ A C_ U. v ) )
20	10 19	sylib	|- ( ph -> E. v ( v C_ Y /\ A C_ U. v ) )
21		vex	|- v e. _V
22	21	a1i	|- ( v C_ Y -> v e. _V )
23		id	|- ( v C_ Y -> v C_ Y )
24	1 22 23	setrec1lem2	|- ( v C_ Y -> U. v e. Y )
25	24	anim1i	|- ( ( v C_ Y /\ A C_ U. v ) -> ( U. v e. Y /\ A C_ U. v ) )
26	25	ancomd	|- ( ( v C_ Y /\ A C_ U. v ) -> ( A C_ U. v /\ U. v e. Y ) )
27	21	uniex	|- U. v e. _V
28		sseq2	|- ( x = U. v -> ( A C_ x <-> A C_ U. v ) )
29		eleq1	|- ( x = U. v -> ( x e. Y <-> U. v e. Y ) )
30	28 29	anbi12d	|- ( x = U. v -> ( ( A C_ x /\ x e. Y ) <-> ( A C_ U. v /\ U. v e. Y ) ) )
31	27 30	spcev	|- ( ( A C_ U. v /\ U. v e. Y ) -> E. x ( A C_ x /\ x e. Y ) )
32	26 31	syl	|- ( ( v C_ Y /\ A C_ U. v ) -> E. x ( A C_ x /\ x e. Y ) )
33	32	exlimiv	|- ( E. v ( v C_ Y /\ A C_ U. v ) -> E. x ( A C_ x /\ x e. Y ) )
34	20 33	syl	|- ( ph -> E. x ( A C_ x /\ x e. Y ) )