Theorem elsetrecs

Description: A set A is an element of setrecs ( F ) iff A is generated by some subset of setrecs ( F ) . The proof requires both setrec1 and setrec2 , but this theorem is not strong enough to uniquely determine setrecs ( F ) . If F respects the subset relation, the theorem still holds if both occurrences of e. are replaced by C_ for a stronger version of the theorem. (Contributed by Emmett Weisz, 12-Jul-2021)

	Ref	Expression
Hypothesis	elsetrecs.1	$$⊢B=\mathrm{setrecs}\left(F\right)$$
Assertion	elsetrecs	$$⊢A\in B\leftrightarrow \exists x\left(x\subseteq B\wedge A\in F\left(x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		elsetrecs.1	$$⊢B=\mathrm{setrecs}\left(F\right)$$
2	1	elsetrecslem	$$⊢A\in B\to \exists x\left(x\subseteq B\wedge A\in F\left(x\right)\right)$$
3		vex	$$⊢x\in \mathrm{V}$$
4	3	a1i	$$⊢x\subseteq B\to x\in \mathrm{V}$$
5		id	$$⊢x\subseteq B\to x\subseteq B$$
6	1 4 5	setrec1	$$⊢x\subseteq B\to F\left(x\right)\subseteq B$$
7	6	sselda	$$⊢\left(x\subseteq B\wedge A\in F\left(x\right)\right)\to A\in B$$
8	7	exlimiv	$$⊢\exists x\left(x\subseteq B\wedge A\in F\left(x\right)\right)\to A\in B$$
9	2 8	impbii	$$⊢A\in B\leftrightarrow \exists x\left(x\subseteq B\wedge A\in F\left(x\right)\right)$$