Theorem elsetrecslem

Description: Lemma for elsetrecs . Any element of setrecs ( F ) is generated by some subset of setrecs ( F ) . This is much weaker than setrec2v . To see why this lemma also requires setrec1 , consider what would happen if we replaced B with { A } . The antecedent would still hold, but the consequent would fail in general. Consider dispensing with the deduction form. (Contributed by Emmett Weisz, 11-Jul-2021) (New usage is discouraged.)

	Ref	Expression
Hypothesis	elsetrecs.1	$$⊢B=\mathrm{setrecs}\left(F\right)$$
Assertion	elsetrecslem	$$⊢A\in B\to \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		ssdifsn	$$⊢B\subseteq B\setminus \left\{A\right\}\leftrightarrow \left(B\subseteq B\wedge \neg A\in B\right)$$
3	2	simprbi	$$⊢B\subseteq B\setminus \left\{A\right\}\to \neg A\in B$$
4	3	con2i	$$⊢A\in B\to \neg B\subseteq B\setminus \left\{A\right\}$$
5		sseq1	$$⊢x=a\to \left(x\subseteq B\leftrightarrow a\subseteq B\right)$$
6		fveq2	$$⊢x=a\to F\left(x\right)=F\left(a\right)$$
7	6	eleq2d	$$⊢x=a\to \left(A\in F\left(x\right)\leftrightarrow A\in F\left(a\right)\right)$$
8	5 7	anbi12d	$$⊢x=a\to \left(\left(x\subseteq B\wedge A\in F\left(x\right)\right)\leftrightarrow \left(a\subseteq B\wedge A\in F\left(a\right)\right)\right)$$
9	8	notbid	$$⊢x=a\to \left(\neg \left(x\subseteq B\wedge A\in F\left(x\right)\right)\leftrightarrow \neg \left(a\subseteq B\wedge A\in F\left(a\right)\right)\right)$$
10	9	spvv	$$⊢\forall x\neg \left(x\subseteq B\wedge A\in F\left(x\right)\right)\to \neg \left(a\subseteq B\wedge A\in F\left(a\right)\right)$$
11		imnan	$$⊢\left(a\subseteq B\to \neg A\in F\left(a\right)\right)\leftrightarrow \neg \left(a\subseteq B\wedge A\in F\left(a\right)\right)$$
12		idd	$$⊢a\subseteq B\to \left(\neg A\in F\left(a\right)\to \neg A\in F\left(a\right)\right)$$
13		vex	$$⊢a\in \mathrm{V}$$
14	13	a1i	$$⊢a\subseteq B\to a\in \mathrm{V}$$
15		id	$$⊢a\subseteq B\to a\subseteq B$$
16	1 14 15	setrec1	$$⊢a\subseteq B\to F\left(a\right)\subseteq B$$
17	12 16	jctild	$$⊢a\subseteq B\to \left(\neg A\in F\left(a\right)\to \left(F\left(a\right)\subseteq B\wedge \neg A\in F\left(a\right)\right)\right)$$
18	17	a2i	$$⊢\left(a\subseteq B\to \neg A\in F\left(a\right)\right)\to \left(a\subseteq B\to \left(F\left(a\right)\subseteq B\wedge \neg A\in F\left(a\right)\right)\right)$$
19	11 18	sylbir	$$⊢\neg \left(a\subseteq B\wedge A\in F\left(a\right)\right)\to \left(a\subseteq B\to \left(F\left(a\right)\subseteq B\wedge \neg A\in F\left(a\right)\right)\right)$$
20	19	adantrd	$$⊢\neg \left(a\subseteq B\wedge A\in F\left(a\right)\right)\to \left(\left(a\subseteq B\wedge \neg A\in a\right)\to \left(F\left(a\right)\subseteq B\wedge \neg A\in F\left(a\right)\right)\right)$$
21		ssdifsn	$$⊢a\subseteq B\setminus \left\{A\right\}\leftrightarrow \left(a\subseteq B\wedge \neg A\in a\right)$$
22		ssdifsn	$$⊢F\left(a\right)\subseteq B\setminus \left\{A\right\}\leftrightarrow \left(F\left(a\right)\subseteq B\wedge \neg A\in F\left(a\right)\right)$$
23	20 21 22	3imtr4g	$$⊢\neg \left(a\subseteq B\wedge A\in F\left(a\right)\right)\to \left(a\subseteq B\setminus \left\{A\right\}\to F\left(a\right)\subseteq B\setminus \left\{A\right\}\right)$$
24	10 23	syl	$$⊢\forall x\neg \left(x\subseteq B\wedge A\in F\left(x\right)\right)\to \left(a\subseteq B\setminus \left\{A\right\}\to F\left(a\right)\subseteq B\setminus \left\{A\right\}\right)$$
25	24	alrimiv	$$⊢\forall x\neg \left(x\subseteq B\wedge A\in F\left(x\right)\right)\to \forall a\left(a\subseteq B\setminus \left\{A\right\}\to F\left(a\right)\subseteq B\setminus \left\{A\right\}\right)$$
26	1 25	setrec2v	$$⊢\forall x\neg \left(x\subseteq B\wedge A\in F\left(x\right)\right)\to B\subseteq B\setminus \left\{A\right\}$$
27	4 26	nsyl	$$⊢A\in B\to \neg \forall x\neg \left(x\subseteq B\wedge A\in F\left(x\right)\right)$$
28		df-ex	$$⊢\exists x\left(x\subseteq B\wedge A\in F\left(x\right)\right)\leftrightarrow \neg \forall x\neg \left(x\subseteq B\wedge A\in F\left(x\right)\right)$$
29	27 28	sylibr	$$⊢A\in B\to \exists x\left(x\subseteq B\wedge A\in F\left(x\right)\right)$$