Theorem setrec1lem1

Description: Lemma for setrec1 . This is a utility theorem showing the equivalence of the statement X e. Y and its expanded form. The proof uses elabg and equivalence theorems.

Variable Y is the class of sets y that are recursively generated by the function F . In other words, y e. Y iff by starting with the empty set and repeatedly applying F to subsets w of our set, we will eventually generate all the elements of Y . In this theorem, X is any element of Y , and V is any class. (Contributed by Emmett Weisz, 16-Oct-2020) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		setrec1lem1.1	|- Y = { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
2		setrec1lem1.2	|- ( ph -> X e. V )
3		sseq2	|- ( y = X -> ( w C_ y <-> w C_ X ) )
4	3	imbi1d	|- ( y = X -> ( ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) <-> ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) ) )
5	4	albidv	|- ( y = X -> ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) <-> A. w ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) ) )
6		sseq1	|- ( y = X -> ( y C_ z <-> X C_ z ) )
7	5 6	imbi12d	|- ( y = X -> ( ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) <-> ( A. w ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> X C_ z ) ) )
8	7	albidv	|- ( y = X -> ( 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 ) ) )
9	8 1	elab2g	|- ( X e. V -> ( X e. Y <-> A. z ( A. w ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> X C_ z ) ) )
10	2 9	syl	|- ( ph -> ( X e. Y <-> A. z ( A. w ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> X C_ z ) ) )