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=\left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
	setrec1lem1.2	$$⊢\phi \to X\in V$$
Assertion	setrec1lem1	$$⊢\phi \to \left(X\in Y\leftrightarrow \forall z\left(\forall w\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to X\subseteq z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		setrec1lem1.1	$$⊢Y=\left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
2		setrec1lem1.2	$$⊢\phi \to X\in V$$
3		sseq2	$$⊢y=X\to \left(w\subseteq y\leftrightarrow w\subseteq X\right)$$
4	3	imbi1d	$$⊢y=X\to \left(\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\leftrightarrow \left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\right)$$
5	4	albidv	$$⊢y=X\to \left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\leftrightarrow \forall w\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\right)$$
6		sseq1	$$⊢y=X\to \left(y\subseteq z\leftrightarrow X\subseteq z\right)$$
7	5 6	imbi12d	$$⊢y=X\to \left(\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\leftrightarrow \left(\forall w\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to X\subseteq z\right)\right)$$
8	7	albidv	$$⊢y=X\to \left(\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\leftrightarrow \forall z\left(\forall w\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to X\subseteq z\right)\right)$$
9	8 1	elab2g	$$⊢X\in V\to \left(X\in Y\leftrightarrow \forall z\left(\forall w\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to X\subseteq z\right)\right)$$
10	2 9	syl	$$⊢\phi \to \left(X\in Y\leftrightarrow \forall z\left(\forall w\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to X\subseteq z\right)\right)$$